1 /-
2 Copyright (c) 2018 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Mario Carneiro
5
6 Godel numbering for partial recursive functions.
7 -/
8 import computability.partrec
src └───────────────────┘
9
10 open encodable denumerable
11
12 namespace nat.partrec
13 open nat (mkpair)
14
15 theorem rfind' {f} (hf : nat.partrec f) : nat.partrec (nat.unpaired (λ a m,
id └─────────┘ ┴ └─────────┘ └──────────┘ ┴ ┴
src └─────────┘ └─────────┘ └──────────┘
typ └─────────┘ ┴ └─────────┘ └──────────┘ ┴ ┴
16 (nat.rfind (λ n, (λ m, m = 0) <$> f (mkpair a (n + m)))).map (+ m))) :=
id └───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └───────┘ ┴ └─┘ └────┘ ┴ └─┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
doc └────┘ └─┘
17 partrec₂.unpaired'.2 $
id └────────────────┘┴
src └────────────────┘┴
typ └────────────────┘┴
18 begin
st └─────
19 refine partrec.map
id └─────────┘
src └─────┘└─────────┘└
typ └─────┘└─────────┘└
doc └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────
20 ((@partrec₂.unpaired' (λ (a b : ℕ),
id └────────────────┘
src ───┘ └────────────────┘┴ └──────┘ └──
typ ───┘ └────────────────┘┴ └──────┘ └──
doc ───┘ ┴ └──────┘ └──
txt ───┘ ┴ └──────┘ └──
par ───┘ ┴ └──────┘ └──
pid ───┘ ┴ └──────┘ └──
st ────────────────────────────────────────
21 nat.rfind (λ n, (λ m, m = 0) <$> f (mkpair a (n + b))))).1 _)
id └───────┘ ┴ └─┘ ┴ └────┘ ┴
src ─────┘└───────┘┴ └──┘ └──┘ ┴┴└──┘└─┘┴ ┴ └────┘┴ ┴ ┴┴┴ └──────────
typ ─────┘└───────┘┴ └──┘ └──┘ ┴┴└──┘└─┘┴┴┴ └────┘┴ ┴ ┴┴┴ └──────────
doc ─────┘ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ └────┘┴ ┴ ┴ ┴ └──────────
txt ─────┘ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────
par ─────┘ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────
pid ─────┘ ┴ └──┘ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────────
st ────────────────────────────────────────────────────────────────────
22 (primrec.nat_add.comp primrec.snd $
id └──────────────────┘
src ───┘ └──────────────────┘┴ ┴ └
typ ───┘ └──────────────────┘┴ ┴ └
doc ───┘ ┴ ┴ └
txt ───┘ ┴ ┴ └
par ───┘ ┴ ┴ └
pid ───┘ ┴ ┴ └
st ────────────────────────────────────────
23 primrec.snd.comp primrec.fst).to_comp.to₂,
id └──────────────┘ └─────────┘
src ─────┘└──────────────┘┴└─────────┘└───────────┘
typ ─────┘└──────────────┘┴└─────────┘└───────────┘
doc ─────┘ ┴ └───────────┘
txt ─────┘ ┴ └───────────┘
par ─────┘ ┴ └───────────┘
pid ─────┘ ┴ └──────────┘┴
st ──────────────────────────────────────────────┘└─
24 have := rfind (partrec₂.unpaired'.2 ((partrec.nat_iff.2 hf).comp
id └───┘ └────────────────┘ └─────────────┘ └┘
src └──────┘└───┘┴ └────────────────┘└─┘ └─────────────┘└─┘ └──────
typ └──────┘└───┘┴ └────────────────┘└─┘ └─────────────┘└─┘└┘└──────
doc └──────┘ ┴ └─┘ └─┘ └──────
txt └──────┘ ┴ └─┘ └─┘ └──────
par └──────┘ ┴ └─┘ └─┘ └──────
pid └───┘└─┘ ┴ └─┘ └─┘ └──────
st ───────────────────────────────────────────────────────────────────
25 (primrec₂.mkpair.comp
id └──────────────────┘
src ───┘ └──────────────────┘└
typ ───┘ └──────────────────┘└
doc ───┘ └
txt ───┘ └
par ───┘ └
pid ───┘ └
st ──────────────────────────
26 (primrec.fst.comp $ primrec.unpair.comp primrec.fst)
id └──────────────┘
src ─────┘ └──────────────┘┴ ┴ ┴ └─
typ ─────┘ └──────────────┘┴ ┴ ┴ └─
doc ─────┘ ┴ ┴ ┴ └─
txt ─────┘ ┴ ┴ ┴ └─
par ─────┘ ┴ ┴ ┴ └─
pid ─────┘ ┴ ┴ ┴ └─
st ───────────────────────────────────────────────────────────
27 (primrec.nat_add.comp primrec.snd
id └──────────────────┘
src ─────┘ └──────────────────┘┴ └
typ ─────┘ └──────────────────┘┴ └
doc ─────┘ ┴ └
txt ─────┘ ┴ └
par ─────┘ ┴ └
pid ─────┘ ┴ └
st ────────────────────────────────────────
28 (primrec.snd.comp $ primrec.unpair.comp primrec.fst))).to_comp).to₂),
id └──────────────┘ └─────────────────┘ └─────────┘
src ───────┘ └──────────────┘┴ ┴└─────────────────┘┴└─────────┘└───────────────┘
typ ───────┘ └──────────────┘┴ ┴└─────────────────┘┴└─────────┘└───────────────┘
doc ───────┘ ┴ ┴ ┴ └───────────────┘
txt ───────┘ ┴ ┴ ┴ └───────────────┘
par ───────┘ ┴ ┴ ┴ └───────────────┘
pid ───────┘ ┴ ┴ ┴ └───────────────┘
st ───────────────────────────────────────────────────────────────────────────┘└─
29 simp at this, exact this
id └──┘
src └──────────┘ └────┘ ┴
typ └──────────┘ └────┘└──┘┴
doc └──────────┘ └────┘ ┴
txt └──────────┘ └────┘ ┴
par └──────────┘ └────┘ ┴
pid ┴└─────┘ ┴ ┴
st ─────────────┘└───────────┘
30 end
st └─┘
31
32 inductive code : Type
33 | zero : code
34 | succ : code
35 | left : code
36 | right : code
37 | pair : code → code → code
38 | comp : code → code → code
39 | prec : code → code → code
40 | rfind' : code → code
41
42 end nat.partrec
43
44 namespace nat.partrec.code
45 open nat (mkpair unpair)
46 open nat.partrec (code)
47
48 instance : inhabited code := ⟨zero⟩
id └───────┘ └──┘ └──┘
src └───────┘ └──┘ └──┘
typ └───────┘ └──┘ └──┘
49
50 protected def const : ℕ → code
id ┴ ┴ └──┘
src ┴ └──┘
typ ┴ ┴ └──┘
51 | 0 := zero
id └──┘
src └──┘
typ └──┘
52 | (n+1) := comp succ (const n)
id ┴┴ └──┘ └──┘ └───┘
src ┴ └──┘ └──┘
typ ┴┴ └──┘ └──┘ └───┘
53
54 protected def id : code := pair left right
id └──┘ └──┘ └──┘ └───┘
src └──┘ └──┘ └──┘ └───┘
typ └──┘ └──┘ └──┘ └───┘
55
56 def curry (c : code) (n : ℕ) : code :=
id └──┘ ┴ └──┘
src └──┘ ┴ └──┘
typ └──┘ ┴ └──┘
57 comp c (pair (code.const n) code.id)
id └──┘ ┴ └──┘ └────────┘ ┴ └─────┘
src └──┘ └──┘ └────────┘ └─────┘
typ └──┘ ┴ └──┘ └────────┘ ┴ └─────┘
58
59 def encode_code : code → ℕ
id └──┘ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴
60 | zero := 0
id └──┘
src └──┘
typ └──┘
61 | succ := 1
id └──┘
src └──┘
typ └──┘
62 | left := 2
id └──┘
src └──┘
typ └──┘
63 | right := 3
id └───┘
src └───┘
typ └───┘
64 | (pair cf cg) := bit0 (bit0 $ mkpair (encode_code cf) (encode_code cg)) + 4
id └──┘ └┘ └┘ └──┘ └──┘ └────┘ └─────────┘ └─────────┘ ┴
src └──┘ └──┘ └──┘ └────┘ ┴
typ └──┘ └┘ └┘ └──┘ └──┘ └────┘ └─────────┘ └─────────┘ ┴
doc └────┘
65 | (comp cf cg) := bit0 (bit1 $ mkpair (encode_code cf) (encode_code cg)) + 4
id └──┘ └┘ └┘ └──┘ └──┘ └────┘ └─────────┘ └─────────┘ ┴
src └──┘ └──┘ └──┘ └────┘ ┴
typ └──┘ └┘ └┘ └──┘ └──┘ └────┘ └─────────┘ └─────────┘ ┴
doc └────┘
66 | (prec cf cg) := bit1 (bit0 $ mkpair (encode_code cf) (encode_code cg)) + 4
id └──┘ └┘ └┘ └──┘ └──┘ └────┘ └─────────┘ └─────────┘ ┴
src └──┘ └──┘ └──┘ └────┘ ┴
typ └──┘ └┘ └┘ └──┘ └──┘ └────┘ └─────────┘ └─────────┘ ┴
doc └────┘
67 | (rfind' cf) := bit1 (bit1 $ encode_code cf) + 4
id └────┘ └┘ └──┘ └──┘ └─────────┘ ┴
src └────┘ └──┘ └──┘ ┴
typ └────┘ └┘ └──┘ └──┘ └─────────┘ ┴
68
69 def of_nat_code : ℕ → code
id ┴ ┴ └──┘
src ┴ └──┘
typ ┴ ┴ └──┘
70 | 0 := zero
id └──┘
src └──┘
typ └──┘
71 | 1 := succ
id └──┘
src └──┘
typ └──┘
72 | 2 := left
id └──┘
src └──┘
typ └──┘
73 | 3 := right
id └───┘
src └───┘
typ └───┘
74 | (n+4) := let m := n.div2.div2 in
id ┴┴ ┴ └────────┘
src ┴ └────────┘
typ ┴┴ ┴ └────────┘
75 have hm : m < n + 4, by simp [m, nat.div2_val];
id ┴ ┴ ┴ ┴ └──────────┘
src ┴ ┴ └────┘ └┘└──────────┘┴
typ ┴ ┴ ┴ └────┘┴└┘└──────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └────────────────────────
76 from lt_of_le_of_lt
id └────────────┘
src └───┘└────────────┘└
typ └───┘└────────────┘└
doc └───┘ └
txt └───┘ └
par └───┘ └
pid └───┘ └
st ──────────────────────
77 (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
id └──────┘ └─────────────┘
src ───┘ └──────┘┴ └────┘ └─────────────┘└──────
typ ───┘ └──────┘┴ └────┘ └─────────────┘└──────
doc ───┘ ┴ └────┘ └──────
txt ───┘ ┴ └────┘ └──────
par ───┘ ┴ └────┘ └──────
pid ───┘ ┴ └────┘ └──────
st ───────────────────────────────────────────────────────────
78 (nat.succ_le_succ (nat.le_add_right _ _)),
id └──────────────┘ └──────────────┘
src ───┘ └──────────────┘┴ └──────────────┘└────┘
typ ───┘ └──────────────┘┴ └──────────────┘└────┘
doc ───┘ ┴ └────┘
txt ───┘ ┴ └────┘
par ───┘ ┴ └────┘
pid ───┘ ┴ └────┘
st ────────────────────────────────────────────┘
79 have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id ┴└─────┘┴ ┴ ┴ └────────────┘ ┴└─────────────┘ └┘
src └─────┘┴ ┴ ┴ └────────────┘ └─────────────┘
typ ┴└─────┘┴ ┴ ┴ └────────────┘ ┴└─────────────┘ └┘
doc └─────┘
80 have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id ┴└─────┘┴ ┴ ┴ └────────────┘ ┴└──────────────┘ └┘
src └─────┘┴ ┴ ┴ └────────────┘ └──────────────┘
typ ┴└─────┘┴ ┴ ┴ └────────────┘ ┴└──────────────┘ └┘
doc └─────┘
81 match n.bodd, n.div2.bodd with
id └───┘ └───┘└───┘
src └───┘ └───┘└───┘
typ └───┘ └───┘└───┘
82 | ff, ff := pair (of_nat_code m.unpair.1) (of_nat_code m.unpair.2)
id └┘ └──┘ └─────────┘ ┴└─────┘┴ └─────────┘ ┴└─────┘┴
src └┘ └──┘ └─────┘┴ └─────┘┴
typ └┘ └──┘ └─────────┘ ┴└─────┘┴ └─────────┘ ┴└─────┘┴
doc └─────┘ └─────┘
83 | ff, tt := comp (of_nat_code m.unpair.1) (of_nat_code m.unpair.2)
id └┘ └┘ └──┘ └─────────┘ ┴└─────┘┴ └─────────┘ ┴└─────┘┴
src └┘ └┘ └──┘ └─────┘┴ └─────┘┴
typ └┘ └┘ └──┘ └─────────┘ ┴└─────┘┴ └─────────┘ ┴└─────┘┴
doc └─────┘ └─────┘
84 | tt, ff := prec (of_nat_code m.unpair.1) (of_nat_code m.unpair.2)
id └┘ └┘ └──┘ └─────────┘ ┴└─────┘┴ └─────────┘ ┴└─────┘┴
src └┘ └┘ └──┘ └─────┘┴ └─────┘┴
typ └┘ └┘ └──┘ └─────────┘ ┴└─────┘┴ └─────────┘ ┴└─────┘┴
doc └─────┘ └─────┘
st └┘
85 | tt, tt := rfind' (of_nat_code m)
id └┘ └────┘ └─────────┘ ┴
src └┘ └────┘
typ └┘ └────┘ └─────────┘ ┴
86 end
87
88 private theorem encode_of_nat_code : ∀ n, encode_code (of_nat_code n) = n
id ┴ └─────────┘ └─────────┘ ┴ ┴ ┴
src └─────────┘ └─────────┘ ┴
typ ┴ └─────────┘ └─────────┘ ┴ ┴ ┴
89 | 0 := rfl
id └─┘
src └─┘
typ └─┘
90 | 1 := rfl
id └─┘
src └─┘
typ └─┘
91 | 2 := rfl
id └─┘
src └─┘
typ └─┘
92 | 3 := rfl
id └─┘
src └─┘
typ └─┘
93 | (n+4) := let m := n.div2.div2 in
id ┴┴ ┴ └────────┘
src ┴ └────────┘
typ ┴┴ ┴ └────────┘
94 have hm : m < n + 4, by simp [m, nat.div2_val];
id ┴ ┴ ┴ ┴ └──────────┘
src ┴ ┴ └────┘ └┘└──────────┘┴
typ ┴ ┴ ┴ └────┘┴└┘└──────────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └────────────────────────
95 from lt_of_le_of_lt
id └────────────┘
src └───┘└────────────┘└
typ └───┘└────────────┘└
doc └───┘ └
txt └───┘ └
par └───┘ └
pid └───┘ └
st ──────────────────────
96 (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
id └──────┘ └─────────────┘
src ───┘ └──────┘┴ └────┘ └─────────────┘└──────
typ ───┘ └──────┘┴ └────┘ └─────────────┘└──────
doc ───┘ ┴ └────┘ └──────
txt ───┘ ┴ └────┘ └──────
par ───┘ ┴ └────┘ └──────
pid ───┘ ┴ └────┘ └──────
st ───────────────────────────────────────────────────────────
97 (nat.succ_le_succ (nat.le_add_right _ _)),
id └──────────────┘ └──────────────┘
src ───┘ └──────────────┘┴ └──────────────┘└────┘
typ ───┘ └──────────────┘┴ └──────────────┘└────┘
doc ───┘ ┴ └────┘
txt ───┘ ┴ └────┘
par ───┘ ┴ └────┘
pid ───┘ ┴ └────┘
st ────────────────────────────────────────────┘
98 have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id ┴└─────┘┴ ┴ ┴ └────────────┘ ┴└─────────────┘ └┘
src └─────┘┴ ┴ ┴ └────────────┘ └─────────────┘
typ ┴└─────┘┴ ┴ ┴ └────────────┘ ┴└─────────────┘ └┘
doc └─────┘
99 have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id ┴└─────┘┴ ┴ ┴ └────────────┘ ┴└──────────────┘ └┘
src └─────┘┴ ┴ ┴ └────────────┘ └──────────────┘
typ ┴└─────┘┴ ┴ ┴ └────────────┘ ┴└──────────────┘ └┘
doc └─────┘
100 have IH : _ := encode_of_nat_code m,
id └────────────────┘ ┴
typ └────────────────┘ ┴
101 have IH1 : _ := encode_of_nat_code m.unpair.1,
id └────────────────┘ ┴└─────┘┴
src └─────┘┴
typ └────────────────┘ ┴└─────┘┴
doc └─────┘
102 have IH2 : _ := encode_of_nat_code m.unpair.2,
id └────────────────┘ ┴└─────┘┴
src └─────┘┴
typ └────────────────┘ ┴└─────┘┴
doc └─────┘
103 begin
st └─────
104 transitivity, swap,
src └──────────┘ └──┘
typ └──────────┘ └──┘
doc └──────────┘ └──┘
txt └──────────┘ └──┘
par └──────────┘ └──┘
st ───────────────┘└────┘└─
105 rw [← nat.bit_decomp n, ← nat.bit_decomp n.div2],
id └────────────┘ ┴ └────────────┘ └────┘
src └────┘└────────────┘┴ └──┘└────────────┘┴└────┘┴
typ └────┘└────────────┘┴┴└──┘└────────────┘┴└────┘┴
doc └────┘ ┴ └──┘ ┴ ┴
txt └────┘ ┴ └──┘ ┴ ┴
par └────┘ ┴ └──┘ ┴ ┴
pid └──┘ ┴ └──┘ ┴ ┴
st ─────────────────────────┘└───────────────────────┘└──
106 simp [encode_code, of_nat_code, -add_comm],
id └─────────┘ └─────────┘
src └────┘└─────────┘└┘└─────────┘└──────────┘
typ └────┘└─────────┘└┘└─────────┘└──────────┘
doc └────┘ └┘ └──────────┘
txt └────┘ └┘ └──────────┘
par └────┘ └┘ └──────────┘
pid ┴┴ └┘ └──────────┘
st ─────────────────────────────────────────────┘└─
107 cases n.bodd; cases n.div2.bodd;
id └────┘ └─────────┘
src └────┘└────┘ └────┘└─────────┘
typ └────┘└────┘ └────┘└─────────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st ─────────────────────────────────────
108 simp [encode_code, of_nat_code, -add_comm, IH, IH1, IH2, m, nat.bit]
id └─────────┘ └─────────┘ └┘ └─┘ └─┘ ┴ └─────┘
src └────┘└─────────┘└┘└─────────┘└───────────┘ └┘ └┘ └┘ └┘└─────┘└─
typ └────┘└─────────┘└┘└─────────┘└───────────┘└┘└┘└─┘└┘└─┘└┘┴└┘└─────┘└─
doc └────┘ └┘ └───────────┘ └┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └───────────┘ └┘ └┘ └┘ └┘ └─
par └────┘ └┘ └───────────┘ └┘ └┘ └┘ └┘ └─
pid ┴┴ └┘ └───────────┘ └┘ └┘ └┘ └┘ ┴└
st ───────────────────────────────────────────────────────────────────────────
109 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
110
111 instance : denumerable code :=
id └─────────┘ └──┘
src └─────────┘ └──┘
typ └─────────┘ └──┘
doc └─────────┘
112 mk' ⟨encode_code, of_nat_code,
id └─┘ └─────────┘ └─────────┘
src └─┘ └─────────┘ └─────────┘
typ └─┘ └─────────┘ └─────────┘
113 λ c, by induction c; try {refl}; simp [
id ┴ ┴
src └────────┘ └───┘└──┘┴ └──────
typ ┴ └────────┘┴ └───┘└──┘┴ └──────
doc └────────┘ └───┘└──┘┴ └──────
txt └────────┘ └───┘└──┘┴ └──────
par └────────┘ └───┘└──┘┴ └──────
pid ┴ └─────┘ ┴└─
st └─────────────────┘└──┘└┘└───────
114 encode_code, of_nat_code, -add_comm, *],
id └─────────┘ └─────────┘
src ───┘└─────────┘└┘└─────────┘└─────────────┘
typ ───┘└─────────┘└┘└─────────┘└─────────────┘
doc ───┘ └┘ └─────────────┘
txt ───┘ └┘ └─────────────┘
par ───┘ └┘ └─────────────┘
pid ───┘ └┘ └─────────────┘
st ──────────────────────────────────────────┘
115 encode_of_nat_code⟩
id └────────────────┘
src └────────────────┘
typ └────────────────┘
116
117 theorem encode_code_eq : encode = encode_code := rfl
id └────┘ ┴ └─────────┘ └─┘
src └────┘ ┴ └─────────┘ └─┘
typ └────┘ ┴ └─────────┘ └─┘
118 theorem of_nat_code_eq : of_nat code = of_nat_code := rfl
id └────┘ └──┘ ┴ └─────────┘ └─┘
src └────┘ └──┘ ┴ └─────────┘ └─┘
typ └────┘ └──┘ ┴ └─────────┘ └─┘
119
120 theorem encode_lt_pair (cf cg) :
121 encode cf < encode (pair cf cg) ∧
id └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘ ┴
src └────┘ ┴ └────┘ └──┘ ┴
typ └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘ ┴
122 encode cg < encode (pair cf cg) :=
id └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘
src └────┘ ┴ └────┘ └──┘
typ └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘
123 begin
st └─────
124 simp [encode_code_eq, encode_code, -add_comm],
id └────────────┘ └─────────┘
src └────┘└────────────┘└┘└─────────┘└──────────┘
typ └────┘└────────────┘└┘└─────────┘└──────────┘
doc └────┘ └┘ └──────────┘
txt └────┘ └┘ └──────────┘
par └────┘ └┘ └──────────┘
pid ┴┴ └┘ └──────────┘
st ──────────────────────────────────────────────┘└─
125 have := nat.mul_le_mul_right _ (dec_trivial : 1 ≤ 2*2),
id └──────────────────┘ └─────────┘ ┴ ┴
src └──────┘└──────────────────┘└─┘ └─────────┘└───┘┴└┘┴└┘
typ └──────┘└──────────────────┘└─┘ └─────────┘└───┘┴└┘┴└┘
doc └──────┘ └─┘ └─────────┘└───┘ └┘ └┘
txt └──────┘ └─┘ └───┘ └┘ └┘
par └──────┘ └─┘ └───┘ └┘ └┘
pid └───┘└─┘ └─┘ └───┘ └┘ └┘
st ───────────────────────────────────────────────────────┘└─
126 rw [one_mul, mul_assoc, ← bit0_eq_two_mul, ← bit0_eq_two_mul] at this,
id └─────┘ └───────┘ └─────────────┘ └─────────────┘
src └──┘└─────┘└┘└───────┘└──┘└─────────────┘└──┘└─────────────┘└───────┘
typ └──┘└─────┘└┘└───────┘└──┘└─────────────┘└──┘└─────────────┘└───────┘
doc └──┘ └┘ └──┘ └──┘ └───────┘
txt └──┘ └┘ └──┘ └──┘ └───────┘
par └──┘ └┘ └──┘ └──┘ └───────┘
pid └┘ └┘ └──┘ └──┘ ┴└──────┘
st ────────────┘└─────────┘└─────────────────┘└─────────────────┘┴└──────┘└─
127 have := lt_of_le_of_lt this (lt_add_of_pos_right _ (dec_trivial:0<4)),
id └────────────┘ └──┘ └─────────────────┘ ┴
src └──────┘└────────────┘┴ ┴ └─────────────────┘└─┘ └┘┴└─┘
typ └──────┘└────────────┘┴└──┘┴ └─────────────────┘└─┘ └┘┴└─┘
doc └──────┘ ┴ ┴ └─┘ └┘ └─┘
txt └──────┘ ┴ ┴ └─┘ └┘ └─┘
par └──────┘ ┴ ┴ └─┘ └┘ └─┘
pid └───┘└─┘ ┴ ┴ └─┘ └┘ └─┘
st ──────────────────────────────────────────────────────────────────────┘└─
128 exact ⟨
src └────┘ └
typ └────┘ └
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ──────────
129 lt_of_le_of_lt (nat.le_mkpair_left _ _) this,
id └────────────────┘
src ───┘ ┴ └────────────────┘└────┘ └─
typ ───┘ ┴ └────────────────┘└────┘ └─
doc ───┘ ┴ └────┘ └─
txt ───┘ ┴ └────┘ └─
par ───┘ ┴ └────┘ └─
pid ───┘ ┴ └────┘ └─
st ──────────────────────────────────────────────────
130 lt_of_le_of_lt (nat.le_mkpair_right _ _) this⟩
id └────────────┘ └─────────────────┘ └──┘
src ───┘└────────────┘┴ └─────────────────┘└────┘ └┘
typ ───┘└────────────┘┴ └─────────────────┘└────┘└──┘└┘
doc ───┘ ┴ └────┘ └┘
txt ───┘ ┴ └────┘ └┘
par ───┘ ┴ └────┘ └┘
pid ───┘ ┴ └────┘ ┴┴
st ──────────────────────────────────────────────────┘
131 end
st └─┘
132
133 theorem encode_lt_comp (cf cg) :
134 encode cf < encode (comp cf cg) ∧
id └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘ ┴
src └────┘ ┴ └────┘ └──┘ ┴
typ └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘ ┴
135 encode cg < encode (comp cf cg) :=
id └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘
src └────┘ ┴ └────┘ └──┘
typ └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘
136 begin
st └─────
137 suffices, exact (encode_lt_pair cf cg).imp
id └────────────┘ └┘ └┘
src └──────┘ └────┘ └────────────┘┴ ┴ └─────
typ └──────┘ └────┘ └────────────┘┴└┘┴└┘└─────
doc └──────┘ └────┘ ┴ ┴ └─────
txt └──────┘ └────┘ ┴ ┴ └─────
par └──────┘ └────┘ ┴ ┴ └─────
pid └──────┘ ┴ ┴ ┴ └─────
st ─────────┘└──────────────────────────────────
138 (λ h, lt_trans h this) (λ h, lt_trans h this),
id └──────┘ └──┘
src ───┘ └──┘ ┴ ┴ └┘ └──┘└──────┘┴ ┴ ┴
typ ───┘ └──┘ ┴ ┴ └┘ └──┘└──────┘┴ ┴└──┘┴
doc ───┘ └──┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
txt ───┘ └──┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
par ───┘ └──┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
pid ───┘ └──┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
st ────────────────────────────────────────────────┘└─
139 change _, simp [encode_code_eq, encode_code, -add_comm],
id └────────────┘ └─────────┘
src └──────┘ └────┘└────────────┘└┘└─────────┘└──────────┘
typ └──────┘ └────┘└────────────┘└┘└─────────┘└──────────┘
doc └──────┘ └────┘ └┘ └──────────┘
txt └──────┘ └────┘ └┘ └──────────┘
par └──────┘ └────┘ └┘ └──────────┘
pid └┘ ┴┴ └┘ └──────────┘
st ────────────────────────────────────────────────────────┘└─
140 exact nat.bit0_lt (nat.lt_succ_self _),
id └─────────┘ └──────────────┘
src └────┘└─────────┘┴ └──────────────┘└─┘
typ └────┘└─────────┘┴ └──────────────┘└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ───────────────────────────────────────┘└─
141 end
st ──┘
142
143 theorem encode_lt_prec (cf cg) :
144 encode cf < encode (prec cf cg) ∧
id └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘ ┴
src └────┘ ┴ └────┘ └──┘ ┴
typ └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘ ┴
145 encode cg < encode (prec cf cg) :=
id └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘
src └────┘ ┴ └────┘ └──┘
typ └────┘ └┘ ┴ └────┘ └──┘ └┘ └┘
146 begin
st └─────
147 suffices, exact (encode_lt_pair cf cg).imp
id └────────────┘ └┘ └┘
src └──────┘ └────┘ └────────────┘┴ ┴ └─────
typ └──────┘ └────┘ └────────────┘┴└┘┴└┘└─────
doc └──────┘ └────┘ ┴ ┴ └─────
txt └──────┘ └────┘ ┴ ┴ └─────
par └──────┘ └────┘ ┴ ┴ └─────
pid └──────┘ ┴ ┴ ┴ └─────
st ─────────┘└──────────────────────────────────
148 (λ h, lt_trans h this) (λ h, lt_trans h this),
id └──────┘ └──┘
src ───┘ └──┘ ┴ ┴ └┘ └──┘└──────┘┴ ┴ ┴
typ ───┘ └──┘ ┴ ┴ └┘ └──┘└──────┘┴ ┴└──┘┴
doc ───┘ └──┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
txt ───┘ └──┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
par ───┘ └──┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
pid ───┘ └──┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
st ────────────────────────────────────────────────┘└─
149 change _, simp [encode_code_eq, encode_code, -add_comm],
id └────────────┘ └─────────┘
src └──────┘ └────┘└────────────┘└┘└─────────┘└──────────┘
typ └──────┘ └────┘└────────────┘└┘└─────────┘└──────────┘
doc └──────┘ └────┘ └┘ └──────────┘
txt └──────┘ └────┘ └┘ └──────────┘
par └──────┘ └────┘ └┘ └──────────┘
pid └┘ ┴┴ └┘ └──────────┘
st ────────────────────────────────────────────────────────┘└─
150 exact nat.lt_succ_self _,
id └──────────────┘
src └────┘└──────────────┘└┘
typ └────┘└──────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ─────────────────────────┘└─
151 end
st ──┘
152
153 theorem encode_lt_rfind' (cf) : encode cf < encode (rfind' cf) :=
id └────┘ └┘ ┴ └────┘ └────┘ └┘
src └────┘ ┴ └────┘ └────┘
typ └────┘ └┘ ┴ └────┘ └────┘ └┘
154 begin
st └─────
155 simp [encode_code_eq, encode_code, -add_comm],
id └────────────┘ └─────────┘
src └────┘└────────────┘└┘└─────────┘└──────────┘
typ └────┘└────────────┘└┘└─────────┘└──────────┘
doc └────┘ └┘ └──────────┘
txt └────┘ └┘ └──────────┘
par └────┘ └┘ └──────────┘
pid ┴┴ └┘ └──────────┘
st ──────────────────────────────────────────────┘└─
156 have := nat.mul_le_mul_right _ (dec_trivial : 1 ≤ 2*2),
id └──────────────────┘ └─────────┘ ┴ ┴
src └──────┘└──────────────────┘└─┘ └─────────┘└───┘┴└┘┴└┘
typ └──────┘└──────────────────┘└─┘ └─────────┘└───┘┴└┘┴└┘
doc └──────┘ └─┘ └─────────┘└───┘ └┘ └┘
txt └──────┘ └─┘ └───┘ └┘ └┘
par └──────┘ └─┘ └───┘ └┘ └┘
pid └───┘└─┘ └─┘ └───┘ └┘ └┘
st ───────────────────────────────────────────────────────┘└─
157 rw [one_mul, mul_assoc, ← bit0_eq_two_mul, ← bit0_eq_two_mul] at this,
id └─────┘ └───────┘ └─────────────┘ └─────────────┘
src └──┘└─────┘└┘└───────┘└──┘└─────────────┘└──┘└─────────────┘└───────┘
typ └──┘└─────┘└┘└───────┘└──┘└─────────────┘└──┘└─────────────┘└───────┘
doc └──┘ └┘ └──┘ └──┘ └───────┘
txt └──┘ └┘ └──┘ └──┘ └───────┘
par └──┘ └┘ └──┘ └──┘ └───────┘
pid └┘ └┘ └──┘ └──┘ ┴└──────┘
st ────────────┘└─────────┘└─────────────────┘└─────────────────┘┴└──────┘└─
158 refine lt_of_le_of_lt (le_trans this _)
id └────────────┘ └──────┘ └──┘
src └─────┘└────────────┘┴ └──────┘┴ └───
typ └─────┘└────────────┘┴ └──────┘┴└──┘└───
doc └─────┘ ┴ ┴ └───
txt └─────┘ ┴ ┴ └───
par └─────┘ ┴ ┴ └───
pid ┴ ┴ ┴ └───
st ──────────────────────────────────────────
159 (lt_add_of_pos_right _ (dec_trivial:0<4)),
id └─────────────────┘ ┴
src ───┘ └─────────────────┘└─┘ └┘┴└─┘
typ ───┘ └─────────────────┘└─┘ └┘┴└─┘
doc ───┘ └─┘ └┘ └─┘
txt ───┘ └─┘ └┘ └─┘
par ───┘ └─┘ └┘ └─┘
pid ───┘ └─┘ └┘ └─┘
st ────────────────────────────────────────────┘└─
160 exact le_of_lt (nat.bit0_lt_bit1 $ le_of_lt $
id └──────┘
src └────┘ ┴ ┴ ┴└──────┘┴ └
typ └────┘ ┴ ┴ ┴└──────┘┴ └
doc └────┘ ┴ ┴ ┴ ┴ └
txt └────┘ ┴ ┴ ┴ ┴ └
par └────┘ ┴ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ └
st ────────────────────────────────────────────────
161 nat.bit0_lt_bit1 $ le_refl _),
id └──────────────┘ └─────┘
src ───┘└──────────────┘┴ ┴└─────┘└─┘
typ ───┘└──────────────┘┴ ┴└─────┘└─┘
doc ───┘ ┴ ┴ └─┘
txt ───┘ ┴ ┴ └─┘
par ───┘ ┴ ┴ └─┘
pid ───┘ ┴ ┴ └─┘
st ────────────────────────────────┘└─
162 end
st ──┘
163
164 section
165 open primrec
166
167 theorem pair_prim : primrec₂ pair :=
id └──────┘ └──┘
src └──────┘ └──┘
typ └──────┘ └──┘
doc └──────┘
168 primrec₂.of_nat_iff.2 $ primrec₂.encode_iff.1 $ nat_add.comp
id └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
src └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
typ └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
169 (nat_bit0.comp $ nat_bit0.comp $
id └──────┘└───┘ └──────┘└───┘
src └──────┘└───┘ └──────┘└───┘
typ └──────┘└───┘ └──────┘└───┘
170 primrec₂.mkpair.comp
id └─────────────┘└───┘
src └─────────────┘└───┘
typ └─────────────┘└───┘
171 (encode_iff.2 $ (primrec.of_nat code).comp fst)
id └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
src └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
typ └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
172 (encode_iff.2 $ (primrec.of_nat code).comp snd))
id └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
src └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
typ └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
173 (primrec₂.const 4)
id └────────────┘
src └────────────┘
typ └────────────┘
174
175 theorem comp_prim : primrec₂ comp :=
id └──────┘ └──┘
src └──────┘ └──┘
typ └──────┘ └──┘
doc └──────┘
176 primrec₂.of_nat_iff.2 $ primrec₂.encode_iff.1 $ nat_add.comp
id └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
src └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
typ └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
177 (nat_bit0.comp $ nat_bit1.comp $
id └──────┘└───┘ └──────┘└───┘
src └──────┘└───┘ └──────┘└───┘
typ └──────┘└───┘ └──────┘└───┘
178 primrec₂.mkpair.comp
id └─────────────┘└───┘
src └─────────────┘└───┘
typ └─────────────┘└───┘
179 (encode_iff.2 $ (primrec.of_nat code).comp fst)
id └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
src └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
typ └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
180 (encode_iff.2 $ (primrec.of_nat code).comp snd))
id └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
src └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
typ └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
181 (primrec₂.const 4)
id └────────────┘
src └────────────┘
typ └────────────┘
182
183 theorem prec_prim : primrec₂ prec :=
id └──────┘ └──┘
src └──────┘ └──┘
typ └──────┘ └──┘
doc └──────┘
184 primrec₂.of_nat_iff.2 $ primrec₂.encode_iff.1 $ nat_add.comp
id └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
src └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
typ └─────────────────┘┴ └─────────────────┘┴ └─────┘└───┘
185 (nat_bit1.comp $ nat_bit0.comp $
id └──────┘└───┘ └──────┘└───┘
src └──────┘└───┘ └──────┘└───┘
typ └──────┘└───┘ └──────┘└───┘
186 primrec₂.mkpair.comp
id └─────────────┘└───┘
src └─────────────┘└───┘
typ └─────────────┘└───┘
187 (encode_iff.2 $ (primrec.of_nat code).comp fst)
id └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
src └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
typ └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
188 (encode_iff.2 $ (primrec.of_nat code).comp snd))
id └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
src └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
typ └────────┘┴ └────────────┘ └──┘ └──┘ └─┘
189 (primrec₂.const 4)
id └────────────┘
src └────────────┘
typ └────────────┘
190
191 theorem rfind_prim : primrec rfind' :=
id └─────┘ └────┘
src └─────┘ └────┘
typ └─────┘ └────┘
doc └─────┘
192 of_nat_iff.2 $ encode_iff.1 $ nat_add.comp
id └────────┘┴ └────────┘┴ └─────┘└───┘
src └────────┘┴ └────────┘┴ └─────┘└───┘
typ └────────┘┴ └────────┘┴ └─────┘└───┘
193 (nat_bit1.comp $ nat_bit1.comp $
id └──────┘└───┘ └──────┘└───┘
src └──────┘└───┘ └──────┘└───┘
typ └──────┘└───┘ └──────┘└───┘
194 encode_iff.2 $ primrec.of_nat code)
id └────────┘┴ └────────────┘ └──┘
src └────────┘┴ └────────────┘ └──┘
typ └────────┘┴ └────────────┘ └──┘
195 (const 4)
id └───┘
src └───┘
typ └───┘
196
197 theorem rec_prim' {α σ} [primcodable α] [primcodable σ]
id └─────────┘ ┴ └─────────┘ ┴
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ ┴
doc └─────────┘ └─────────┘
198 {c : α → code} (hc : primrec c)
id ┴ └──┘ └─────┘ ┴
src └──┘ └─────┘
typ ┴ └──┘ └─────┘ ┴
doc └─────┘
199 {z : α → σ} (hz : primrec z)
id ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴
doc └─────┘
200 {s : α → σ} (hs : primrec s)
id ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴
doc └─────┘
201 {l : α → σ} (hl : primrec l)
id ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴
doc └─────┘
202 {r : α → σ} (hr : primrec r)
id ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴
doc └─────┘
203 {pr : α → code × code × σ × σ → σ} (hpr : primrec₂ pr)
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘
src └──┘ ┴ └──┘ ┴ ┴ └──────┘
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘
doc └──────┘
204 {co : α → code × code × σ × σ → σ} (hco : primrec₂ co)
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘
src └──┘ ┴ └──┘ ┴ ┴ └──────┘
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘
doc └──────┘
205 {pc : α → code × code × σ × σ → σ} (hpc : primrec₂ pc)
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘
src └──┘ ┴ └──┘ ┴ ┴ └──────┘
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ └──────┘ └┘
doc └──────┘
206 {rf : α → code × σ → σ} (hrf : primrec₂ rf) :
id ┴ └──┘ ┴ ┴ ┴ └──────┘ └┘
src └──┘ ┴ └──────┘
typ ┴ └──┘ ┴ ┴ ┴ └──────┘ └┘
doc └──────┘
207 let PR (a) := λ cf cg hf hg, pr a (cf, cg, hf, hg),
id └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ ┴└┘ └┘ └┘ └┘
src ┴
typ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ ┴└┘ └┘ └┘ └┘
208 CO (a) := λ cf cg hf hg, co a (cf, cg, hf, hg),
id └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ ┴└┘ └┘ └┘ └┘
src ┴
typ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ ┴└┘ └┘ └┘ └┘
209 PC (a) := λ cf cg hf hg, pc a (cf, cg, hf, hg),
id └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ ┴└┘ └┘ └┘ └┘
src ┴
typ └┘ ┴ └┘ └┘ └┘ └┘ └┘ ┴ ┴└┘ └┘ └┘ └┘
210 RF (a) := λ cf hf, rf a (cf, hf),
id └┘ ┴ └┘ └┘ └┘ ┴ ┴└┘ └┘
src ┴
typ └┘ ┴ └┘ └┘ └┘ ┴ ┴└┘ └┘
211 F (a c) : σ := nat.partrec.code.rec_on c
id ┴ ┴ ┴ └─────────────────────┘ ┴
src └─────────────────────┘
typ ┴ ┴ ┴ └─────────────────────┘ ┴
212 (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴
213 primrec (λ a, F a (c a)) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
214 begin
st └─────
215 intros,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
216 let G₁ : (α × list σ) × ℕ × ℕ → option σ := λ p,
id ┴ ┴ └──┘ ┴ └────┘ ┴
src └───────┘ ┴┴┴└──┘┴ └┘ ┴ ┴ ┴ ┴ ┴└────┘┴ └──┘ └───
typ └───────┘ ┴┴┴┴└──┘┴ └┘┴┴ ┴ ┴ ┴ ┴└────┘┴┴└──┘ └───
doc └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───
txt └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───
par └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───
pid └────┘└─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └───
st ───────────────────────────────────────────────────
217 let a := p.1.1, IH := p.1.2, n := p.2.1, m := p.2.2 in
src ───┘ └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
typ ───┘ └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
doc ───┘ └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
txt ───┘ └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
par ───┘ └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
pid ───┘ └────┘ └──────────┘ └─────────┘ └─────────┘ └───────
st ───────────────────────────────────────────────────────────
218 (IH.nth m).bind $ λ s,
id └──┘
src ───┘ └──┘┴ └─────┘ ┴ └───
typ ───┘ └──┘┴ └─────┘ ┴ └───
doc ───┘ ┴ └─────┘ ┴ └───
txt ───┘ ┴ └─────┘ ┴ └───
par ───┘ ┴ └─────┘ ┴ └───
pid ───┘ ┴ └─────┘ ┴ └───
st ───────────────────────────
219 (IH.nth m.unpair.1).bind $ λ s₁,
id └──┘ └─────┘
src ───┘ └──┘┴ └─────┘└───────┘ ┴ └────
typ ───┘ └──┘┴ └─────┘└───────┘ ┴ └────
doc ───┘ ┴ └─────┘└───────┘ ┴ └────
txt ───┘ ┴ └───────┘ ┴ └────
par ───┘ ┴ └───────┘ ┴ └────
pid ───┘ ┴ └───────┘ ┴ └────
st ─────────────────────────────────────
220 (IH.nth m.unpair.2).map $ λ s₂,
id └──┘ └─────┘
src ───┘ └──┘┴ └─────┘└──────┘ ┴ └────
typ ───┘ └──┘┴ └─────┘└──────┘ ┴ └────
doc ───┘ ┴ └─────┘└──────┘ ┴ └────
txt ───┘ ┴ └──────┘ ┴ └────
par ───┘ ┴ └──────┘ ┴ └────
pid ───┘ ┴ └──────┘ ┴ └────
st ────────────────────────────────────
221 cond n.bodd
id └───┘
src ───┘ ┴ └───┘└
typ ───┘ ┴ └───┘└
doc ───┘ ┴ └
txt ───┘ ┴ └
par ───┘ ┴ └
pid ───┘ ┴ └
st ────────────────
222 (cond n.div2.bodd
id └───┘└───┘
src ─────┘ ┴ └───┘└───┘└
typ ─────┘ ┴ └───┘└───┘└
doc ─────┘ ┴ └
txt ─────┘ ┴ └
par ─────┘ ┴ └
pid ─────┘ ┴ └
st ────────────────────────
223 (rf a (of_nat code m, s))
id └┘
src ───────┘ ┴ ┴ ┴ ┴ └┘ └──
typ ───────┘ └┘┴ ┴ ┴ ┴ └┘ └──
doc ───────┘ ┴ ┴ ┴ ┴ └┘ └──
txt ───────┘ ┴ ┴ ┴ ┴ └┘ └──
par ───────┘ ┴ ┴ ┴ ┴ └┘ └──
pid ───────┘ ┴ ┴ ┴ ┴ └┘ └──
st ──────────────────────────────────
224 (pc a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂)))
id └┘ └─────┘
src ───────┘ ┴ ┴ ┴ ┴ └─────┘└──┘ ┴ ┴ └──┘ └┘ └───
typ ───────┘ └┘┴ ┴ ┴ ┴ └─────┘└──┘ ┴ ┴ └──┘ └┘ └───
doc ───────┘ ┴ ┴ ┴ ┴ └─────┘└──┘ ┴ ┴ └──┘ └┘ └───
txt ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └───
par ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └───
pid ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └───
st ─────────────────────────────────────────────────────────────────────────
225 (cond n.div2.bodd
id └──┘
src ─────┘ └──┘┴ └
typ ─────┘ └──┘┴ └
doc ─────┘ ┴ └
txt ─────┘ ┴ └
par ─────┘ ┴ └
pid ─────┘ ┴ └
st ────────────────────────
226 (co a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂))
id └┘
src ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └──
typ ───────┘ └┘┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └──
doc ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └──
txt ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └──
par ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └──
pid ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └──
st ────────────────────────────────────────────────────────────────────────
227 (pr a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂))),
id └┘ └────┘ └──┘
src ───────┘ ┴ ┴ ┴ ┴ └──┘└────┘┴└──┘┴ └──┘ └┘ └─┘
typ ───────┘ └┘┴ ┴ ┴ ┴ └──┘└────┘┴└──┘┴ └──┘ └┘ └─┘
doc ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └─┘
txt ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └─┘
par ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └─┘
pid ───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘ └─┘
st ───────────────────────────────────────────────────────────────────────┘└─
228 have : primrec G₁,
id └─────┘ └┘
src └─────┘└─────┘┴
typ └─────┘└─────┘┴└┘
doc └─────┘└─────┘┴
txt └─────┘ ┴
par └─────┘ ┴
pid └───┘└┘ ┴
st ──────────────────┘└─
229 { refine option_bind (list_nth.comp (snd.comp fst) (snd.comp snd)) _,
id └─────────┘ └───────────┘ └─┘ └──────┘ └─┘
src └─────┘└─────────┘┴ └───────────┘┴ ┴└─┘└┘ └──────┘┴└─┘└──┘
typ └─────┘└─────────┘┴ └───────────┘┴ ┴└─┘└┘ └──────┘┴└─┘└──┘
doc └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ └──┘
pid ┴ ┴ ┴ ┴ └┘ ┴ └──┘
st ───┘└────────────────────────────────────────────────────────────────┘└─
230 refine option_bind ((list_nth.comp (snd.comp fst)
id └─────────┘ └───────────┘
src └─────┘└─────────┘┴ └───────────┘┴ ┴ └─
typ └─────┘└─────────┘┴ └───────────┘┴ ┴ └─
doc └─────┘ ┴ ┴ ┴ └─
txt └─────┘ ┴ ┴ ┴ └─
par └─────┘ ┴ ┴ ┴ └─
pid ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────────────────
231 (fst.comp $ primrec.unpair.comp (snd.comp snd))).comp fst) _,
id └──────┘ └─────────────────┘ └──────┘ └─┘ └─┘
src ─────┘ └──────┘┴ ┴└─────────────────┘┴ └──────┘┴└─┘└───────┘└─┘└─┘
typ ─────┘ └──────┘┴ ┴└─────────────────┘┴ └──────┘┴└─┘└───────┘└─┘└─┘
doc ─────┘ ┴ ┴ ┴ ┴ └───────┘ └─┘
txt ─────┘ ┴ ┴ ┴ ┴ └───────┘ └─┘
par ─────┘ ┴ ┴ ┴ ┴ └───────┘ └─┘
pid ─────┘ ┴ ┴ ┴ ┴ └───────┘ └─┘
st ─────────────────────────────────────────────────────────────────┘└─
232 refine option_map ((list_nth.comp (snd.comp fst)
id └────────┘ └───────────┘
src └─────┘└────────┘┴ └───────────┘┴ ┴ └─
typ └─────┘└────────┘┴ └───────────┘┴ ┴ └─
doc └─────┘ ┴ ┴ ┴ └─
txt └─────┘ ┴ ┴ ┴ └─
par └─────┘ ┴ ┴ ┴ └─
pid ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────────
233 (snd.comp $ primrec.unpair.comp (snd.comp snd))).comp $ fst.comp fst) _,
id └─────────────────┘ └──────┘ └─┘ └──────┘ └─┘
src ─────┘ ┴ ┴└─────────────────┘┴ └──────┘┴└─┘└───────┘ ┴└──────┘┴└─┘└─┘
typ ─────┘ ┴ ┴└─────────────────┘┴ └──────┘┴└─┘└───────┘ ┴└──────┘┴└─┘└─┘
doc ─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘
txt ─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘
par ─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘
pid ─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────────┘└─
234 have a := fst.comp (fst.comp $ fst.comp $ fst.comp fst),
id └──────┘ └─┘
src └────────┘ ┴ ┴ ┴ ┴ ┴└──────┘┴└─┘┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴└──────┘┴└─┘┴
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └────┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
235 have n := fst.comp (snd.comp $ fst.comp $ fst.comp fst),
id └──────┘ └──────┘ └─┘
src └────────┘ ┴ └──────┘┴ ┴ ┴ ┴└──────┘┴└─┘┴
typ └────────┘ ┴ └──────┘┴ ┴ ┴ ┴└──────┘┴└─┘┴
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └────┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
236 have m := snd.comp (snd.comp $ fst.comp $ fst.comp fst),
id └──────┘ └──────┘ └─┘
src └────────┘ ┴ └──────┘┴ ┴ ┴ ┴└──────┘┴└─┘┴
typ └────────┘ ┴ └──────┘┴ ┴ ┴ ┴└──────┘┴└─┘┴
doc └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └────┘┴└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
237 have m₁ := fst.comp (primrec.unpair.comp m),
id └──────┘ └─────────────────┘ ┴
src └─────────┘└──────┘┴ └─────────────────┘┴ ┴
typ └─────────┘└──────┘┴ └─────────────────┘┴┴┴
doc └─────────┘ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
238 have m₂ := snd.comp (primrec.unpair.comp m),
id └──────┘ └─────────────────┘ ┴
src └─────────┘└──────┘┴ └─────────────────┘┴ ┴
typ └─────────┘└──────┘┴ └─────────────────┘┴┴┴
doc └─────────┘ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────┘└─
239 have s := snd.comp (fst.comp fst),
id └──────┘ └──────┘ └─┘
src └────────┘└──────┘┴ └──────┘┴└─┘┴
typ └────────┘└──────┘┴ └──────┘┴└─┘┴
doc └────────┘ ┴ ┴ ┴
txt └────────┘ ┴ ┴ ┴
par └────────┘ ┴ ┴ ┴
pid └────┘┴└─┘ ┴ ┴ ┴
st ────────────────────────────────────┘└─
240 have s₁ := snd.comp fst,
id └──────┘ └─┘
src └─────────┘└──────┘┴└─┘
typ └─────────┘└──────┘┴└─┘
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid └─────┘┴└─┘ ┴
st ──────────────────────────┘
241 have s₂ := snd,
242 exact (nat_bodd.comp n).cond
243 ((nat_bodd.comp $ nat_div2.comp n).cond
244 (hrf.comp a (((primrec.of_nat code).comp m).pair s))
245 (hpc.comp a (((primrec.of_nat code).comp m₁).pair $
246 ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂)))
247 (primrec.cond (nat_bodd.comp $ nat_div2.comp n)
248 (hco.comp a (((primrec.of_nat code).comp m₁).pair $
249 ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂))
250 (hpr.comp a (((primrec.of_nat code).comp m₁).pair $
251 ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂))) },
id └──┘
src └──┘
typ └──┘
st └┘
252 let G : α → list σ → option σ := λ a IH,
id ┴ └──┘ └────┘ ┴ ┴ └┘
src └──┘ └────┘
typ ┴ └──┘ └────┘ ┴ ┴ └┘
253 IH.length.cases (some (z a)) $ λ n,
id ┴ ┴
typ ┴ ┴
254 n.cases (some (s a)) $ λ n,
id ┴ ┴
typ ┴ ┴
255 n.cases (some (l a)) $ λ n,
id ┴ ┴
typ ┴ ┴
256 n.cases (some (r a)) $ λ n,
id ┴ ┴
typ ┴ ┴
257 G₁ ((a, IH), n, n.div2.div2),
id └────────┘
src └────────┘
typ └────────┘
258 have : primrec₂ G := (nat_cases
259 (list_length.comp snd) (option_some_iff.2 (hz.comp fst)) $
260 nat_cases snd (option_some_iff.2 (hs.comp (fst.comp fst))) $
261 nat_cases snd (option_some_iff.2 (hl.comp (fst.comp $ fst.comp fst))) $
262 nat_cases snd (option_some_iff.2 (hr.comp (fst.comp $ fst.comp $ fst.comp fst)))
263 (this.comp $
264 ((fst.pair snd).comp $ fst.comp $ fst.comp $ fst.comp $ fst).pair $
265 snd.pair $ nat_div2.comp $ nat_div2.comp snd)),
266 refine ((nat_strong_rec
267 (λ a n, F a (of_nat code n)) this.to₂ $ λ a n, _).comp
id ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴
268 primrec.id $ encode_iff.2 hc).of_eq (λ a, by simp),
id ┴
typ ┴
269 simp,
270 iterate 4 {cases n with n, {refl}},
id ┴
typ ┴
st ┴
271 simp [G], rw [list.length_map, list.length_range],
272 let m := n.div2.div2,
id └─────────┘
src └─────────┘
typ └─────────┘
273 show G₁ ((a, (list.range (n+4)).map (λ n, F a (of_nat code n))), n, m)
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
274 = some (F a (of_nat code (n+4))),
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
275 have hm : m < n + 4, by simp [nat.div2_val, m];
id ┴ ┴ ┴
typ ┴ ┴ ┴
276 from lt_of_le_of_lt
277 (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
278 (nat.succ_le_succ (nat.le_add_right _ _)),
279 have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
280 have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
281 simp [G₁], simp [list.nth_map, list.nth_range, hm, m1, m2],
282 change of_nat code (n+4) with of_nat_code (n+4),
id └──┘ ┴ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ ┴ └─────────┘ ┴
283 simp [of_nat_code],
id └─────────┘
src └─────────┘
typ └─────────┘
284 cases n.bodd; cases n.div2.bodd; refl
id └────┘ └──┘
src └────┘ └──┘
typ └────┘ └──┘
doc └──┘
285 end
st └─┘
286
287 theorem rec_prim {α σ} [primcodable α] [primcodable σ]
id └──┘ └──┘ ┴ ┴ └┘ └┘ └┘ ┴
src └──┘ └──┘ ┴ └┘ └┘ └┘
typ └──┘ └──┘ ┴ ┴ └┘ └┘ └┘ ┴
doc └──┘ └──┘ ┴ └┘ └┘ └┘
288 {c : α → code} (hc : primrec c)
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
289 {z : α → σ} (hz : primrec z)
id ┴ ┴ ┴
typ ┴ ┴ ┴
290 {s : α → σ} (hs : primrec s)
id ┴ ┴ ┴
typ ┴ ┴ ┴
291 {l : α → σ} (hl : primrec l)
id ┴ ┴
typ ┴ ┴
292 {r : α → σ} (hr : primrec r)
id ┴ ┴ ┴
typ ┴ ┴ ┴
293 {pr : α → code → code → σ → σ → σ}
id ┴ └──┘ └──┘ ┴ ┴ ┴
src └──┘ └──┘
typ ┴ └──┘ └──┘ ┴ ┴ ┴
294 (hpr : primrec (λ a : α × code × code × σ × σ,
id ┴ └──┘ └──┘ ┴ ┴
src └──┘ └──┘
typ ┴ └──┘ └──┘ ┴ ┴
295 pr a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2))
296 {co : α → code → code → σ → σ → σ}
id ┴ └──┘ └──┘ ┴ ┴ ┴
src └──┘ └──┘
typ ┴ └──┘ └──┘ ┴ ┴ ┴
297 (hco : primrec (λ a : α × code × code × σ × σ,
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ └──┘ ┴
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴
298 co a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2))
299 {pc : α → code → code → σ → σ → σ}
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
300 (hpc : primrec (λ a : α × code × code × σ × σ,
id ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘ ┴ └──┘ ┴ ┴
typ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ ┴
301 pc a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2))
302 {rf : α → code → σ → σ}
id ┴ └──┘ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴
303 (hrf : primrec (λ a : α × code × σ, rf a.1 a.2.1 a.2.2)) :
id ┴ └──┘ ┴ ┴ └┘
src └──┘ ┴
typ ┴ └──┘ ┴ ┴ └┘
304 let F (a c) : σ := nat.partrec.code.rec_on c
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
305 (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a) in
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
306 primrec (λ a, F a (c a)) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
307 begin
308 intros,
309 let G₁ : (α × list σ) × ℕ × ℕ → option σ := λ p,
id ┴ └──┘ └────┘ ┴
src └──┘ └────┘
typ ┴ └──┘ └────┘ ┴
310 let a := p.1.1, IH := p.1.2, n := p.2.1, m := p.2.2 in
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
311 (IH.nth m).bind $ λ s,
id ┴
typ ┴
312 (IH.nth m.unpair.1).bind $ λ s₁,
id └─────┘ └┘
src └─────┘
typ └─────┘ └┘
doc └─────┘
313 (IH.nth m.unpair.2).map $ λ s₂,
id └─────┘ └┘
src └─────┘
typ └─────┘ └┘
doc └─────┘
314 cond n.bodd
id └───┘
src └───┘
typ └───┘
315 (cond n.div2.bodd
id └───┘└───┘
src └───┘└───┘
typ └───┘└───┘
316 (rf a (of_nat code m) s)
id └┘
typ └┘
317 (pc a (of_nat code m.unpair.1) (of_nat code m.unpair.2) s₁ s₂))
318 (cond n.div2.bodd
319 (co a (of_nat code m.unpair.1) (of_nat code m.unpair.2) s₁ s₂)
320 (pr a (of_nat code m.unpair.1) (of_nat code m.unpair.2) s₁ s₂)),
id └──┘
src └──┘
typ └──┘
321 have : primrec G₁,
322 { refine option_bind (list_nth.comp (snd.comp fst) (snd.comp snd)) _,
323 refine option_bind ((list_nth.comp (snd.comp fst)
324 (fst.comp $ primrec.unpair.comp (snd.comp snd))).comp fst) _,
325 refine option_map ((list_nth.comp (snd.comp fst)
326 (snd.comp $ primrec.unpair.comp (snd.comp snd))).comp $ fst.comp fst) _,
327 have a := fst.comp (fst.comp $ fst.comp $ fst.comp fst),
328 have n := fst.comp (snd.comp $ fst.comp $ fst.comp fst),
329 have m := snd.comp (snd.comp $ fst.comp $ fst.comp fst),
330 have m₁ := fst.comp (primrec.unpair.comp m),
331 have m₂ := snd.comp (primrec.unpair.comp m),
332 have s := snd.comp (fst.comp fst),
333 have s₁ := snd.comp fst,
334 have s₂ := snd,
335 exact (nat_bodd.comp n).cond
336 ((nat_bodd.comp $ nat_div2.comp n).cond
337 (hrf.comp $ a.pair (((primrec.of_nat code).comp m).pair s))
338 (hpc.comp $ a.pair (((primrec.of_nat code).comp m₁).pair $
339 ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂)))
340 (primrec.cond (nat_bodd.comp $ nat_div2.comp n)
341 (hco.comp $ a.pair (((primrec.of_nat code).comp m₁).pair $
342 ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂))
343 (hpr.comp $ a.pair (((primrec.of_nat code).comp m₁).pair $
344 ((primrec.of_nat code).comp m₂).pair $ s₁.pair s₂))) },
id └──┘
src └──┘
typ └──┘
st └┘
345 let G : α → list σ → option σ := λ a IH,
id ┴ └──┘ └────┘ ┴ ┴ └┘
src └──┘ └────┘
typ ┴ └──┘ └────┘ ┴ ┴ └┘
346 IH.length.cases (some (z a)) $ λ n,
id ┴ ┴
typ ┴ ┴
347 n.cases (some (s a)) $ λ n,
id ┴ ┴
typ ┴ ┴
348 n.cases (some (l a)) $ λ n,
id ┴ ┴
typ ┴ ┴
349 n.cases (some (r a)) $ λ n,
id ┴ ┴
typ ┴ ┴
350 G₁ ((a, IH), n, n.div2.div2),
id └────────┘
src └────────┘
typ └────────┘
351 have : primrec₂ G := (nat_cases
352 (list_length.comp snd) (option_some_iff.2 (hz.comp fst)) $
353 nat_cases snd (option_some_iff.2 (hs.comp (fst.comp fst))) $
354 nat_cases snd (option_some_iff.2 (hl.comp (fst.comp $ fst.comp fst))) $
355 nat_cases snd (option_some_iff.2 (hr.comp (fst.comp $ fst.comp $ fst.comp fst)))
356 (this.comp $
357 ((fst.pair snd).comp $ fst.comp $ fst.comp $ fst.comp $ fst).pair $
358 snd.pair $ nat_div2.comp $ nat_div2.comp snd)),
359 refine ((nat_strong_rec
360 (λ a n, F a (of_nat code n)) this.to₂ $ λ a n, _).comp
id ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴
361 primrec.id $ encode_iff.2 hc).of_eq (λ a, by simp),
id ┴
typ ┴
362 simp,
363 iterate 4 {cases n with n, {refl}},
id ┴
typ ┴
st ┴
364 simp [G], rw [list.length_map, list.length_range],
365 let m := n.div2.div2,
id └─────────┘
src └─────────┘
typ └─────────┘
366 show G₁ ((a, (list.range (n+4)).map (λ n, F a (of_nat code n))), n, m)
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
367 = some (F a (of_nat code (n+4))),
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
368 have hm : m < n + 4, by simp [nat.div2_val, m];
id ┴ ┴ ┴
typ ┴ ┴ ┴
369 from lt_of_le_of_lt
370 (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
371 (nat.succ_le_succ (nat.le_add_right _ _)),
372 have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
373 have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
374 simp [G₁], simp [list.nth_map, list.nth_range, hm, m1, m2],
375 change of_nat code (n+4) with of_nat_code (n+4),
id └──┘ ┴ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ ┴ └─────────┘ ┴
376 simp [of_nat_code],
id └─────────┘
src └─────────┘
typ └─────────┘
377 cases n.bodd; cases n.div2.bodd; refl
id └────┘ └──┘
src └────┘ └──┘
typ └────┘ └──┘
doc └──┘
378 end
st └─┘
379
380 end
381
382 section
383 open computable
384
385 /- TODO(Mario): less copy-paste from previous proof -/
386 theorem rec_computable {α σ} [primcodable α] [primcodable σ]
id └┘ └──┘ ┴ └──┘ └──┘ ┴
src └┘ └──┘ ┴ └──┘ └──┘
typ └┘ └──┘ ┴ └──┘ └──┘ ┴
doc └┘ └──┘ ┴ └──┘ └──┘
387 {c : α → code} (hc : computable c)
id ┴ └─┘
src └─┘
typ ┴ └─┘
388 {z : α → σ} (hz : computable z)
id ┴ ┴ ┴
typ ┴ ┴ ┴
389 {s : α → σ} (hs : computable s)
id ┴ ┴ ┴
typ ┴ ┴ ┴
390 {l : α → σ} (hl : computable l)
id ┴ ┴
typ ┴ ┴
391 {r : α → σ} (hr : computable r)
id ┴ ┴ ┴
typ ┴ ┴ ┴
392 {pr : α → code × code × σ × σ → σ} (hpr : computable₂ pr)
id ┴ └──┘ └──┘ ┴ ┴ ┴
src └──┘ └──┘
typ ┴ └──┘ └──┘ ┴ ┴ ┴
393 {co : α → code × code × σ × σ → σ} (hco : computable₂ co)
id └──┘ └──┘ ┴ ┴ ┴
src └──┘ └──┘
typ └──┘ └──┘ ┴ ┴ ┴
394 {pc : α → code × code × σ × σ → σ} (hpc : computable₂ pc)
id ┴ └──┘ └─┘ ┴ ┴ ┴ ┴
src └──┘ └─┘ ┴
typ ┴ └──┘ └─┘ ┴ ┴ ┴ ┴
395 {rf : α → code × σ → σ} (hrf : computable₂ rf) :
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
396 let PR (a) := λ cf cg hf hg, pr a (cf, cg, hf, hg),
id ┴ └┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ └┘
typ ┴ └┘ ┴ └┘ └┘ ┴ ┴ └┘ └┘ └┘
397 CO (a) := λ cf cg hf hg, co a (cf, cg, hf, hg),
id ┴ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘
398 PC (a) := λ cf cg hf hg, pc a (cf, cg, hf, hg),
id ┴ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘
399 RF (a) := λ cf hf, rf a (cf, hf),
id └┘ ┴ └┘ └┘ ┴ └┘ └┘
typ └┘ ┴ └┘ └┘ ┴ └┘ └┘
400 F (a c) : σ := nat.partrec.code.rec_on c
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
401 (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
402 computable (λ a, F a (c a)) :=
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
403 begin
404 intros,
405 let G₁ : (α × list σ) × ℕ × ℕ → option σ := λ p,
id ┴ └──┘ └────┘ ┴
src └──┘ └────┘
typ ┴ └──┘ └────┘ ┴
406 let a := p.1.1, IH := p.1.2, n := p.2.1, m := p.2.2 in
id ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ ┴
407 (IH.nth m).bind $ λ s,
id ┴
typ ┴
408 (IH.nth m.unpair.1).bind $ λ s₁,
id └─────┘ └┘
src └─────┘
typ └─────┘ └┘
doc └─────┘
409 (IH.nth m.unpair.2).map $ λ s₂,
id └─────┘ └┘
src └─────┘
typ └─────┘ └┘
doc └─────┘
410 cond n.bodd
id └───┘
src └───┘
typ └───┘
411 (cond n.div2.bodd
id └───┘└───┘
src └───┘└───┘
typ └───┘└───┘
412 (rf a (of_nat code m, s))
413 (pc a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂)))
414 (cond n.div2.bodd
415 (co a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂))
416 (pr a (of_nat code m.unpair.1, of_nat code m.unpair.2, s₁, s₂))),
id └──┘
src └──┘
typ └──┘
417 have : computable G₁,
418 { refine option_bind (list_nth.comp (snd.comp fst) (snd.comp snd)) _,
419 refine option_bind ((list_nth.comp (snd.comp fst)
420 (fst.comp $ computable.unpair.comp (snd.comp snd))).comp fst) _,
421 refine option_map ((list_nth.comp (snd.comp fst)
422 (snd.comp $ computable.unpair.comp (snd.comp snd))).comp $ fst.comp fst) _,
423 have a := fst.comp (fst.comp $ fst.comp $ fst.comp fst),
424 have n := fst.comp (snd.comp $ fst.comp $ fst.comp fst),
425 have m := snd.comp (snd.comp $ fst.comp $ fst.comp fst),
426 have m₁ := fst.comp (computable.unpair.comp m),
427 have m₂ := snd.comp (computable.unpair.comp m),
428 have s := snd.comp (fst.comp fst),
429 have s₁ := snd.comp fst,
430 have s₂ := snd,
431 exact (nat_bodd.comp n).cond
432 ((nat_bodd.comp $ nat_div2.comp n).cond
433 (hrf.comp a (((computable.of_nat code).comp m).pair s))
434 (hpc.comp a (((computable.of_nat code).comp m₁).pair $
435 ((computable.of_nat code).comp m₂).pair $ s₁.pair s₂)))
436 (computable.cond (nat_bodd.comp $ nat_div2.comp n)
437 (hco.comp a (((computable.of_nat code).comp m₁).pair $
438 ((computable.of_nat code).comp m₂).pair $ s₁.pair s₂))
439 (hpr.comp a (((computable.of_nat code).comp m₁).pair $
440 ((computable.of_nat code).comp m₂).pair $ s₁.pair s₂))) },
id └──┘
src └──┘
typ └──┘
st └┘
441 let G : α → list σ → option σ := λ a IH,
id ┴ └──┘ └────┘ ┴ ┴ └┘
src └──┘ └────┘
typ ┴ └──┘ └────┘ ┴ ┴ └┘
442 IH.length.cases (some (z a)) $ λ n,
id ┴ ┴
typ ┴ ┴
443 n.cases (some (s a)) $ λ n,
id ┴ ┴
typ ┴ ┴
444 n.cases (some (l a)) $ λ n,
id ┴ ┴
typ ┴ ┴
445 n.cases (some (r a)) $ λ n,
id ┴ ┴
typ ┴ ┴
446 G₁ ((a, IH), n, n.div2.div2),
id └────────┘
src └────────┘
typ └────────┘
447 have : computable₂ G := (nat_cases
448 (list_length.comp snd) (option_some_iff.2 (hz.comp fst)) $
449 nat_cases snd (option_some_iff.2 (hs.comp (fst.comp fst))) $
450 nat_cases snd (option_some_iff.2 (hl.comp (fst.comp $ fst.comp fst))) $
451 nat_cases snd (option_some_iff.2 (hr.comp (fst.comp $ fst.comp $ fst.comp fst)))
452 (this.comp $
453 ((fst.pair snd).comp $ fst.comp $ fst.comp $ fst.comp $ fst).pair $
454 snd.pair $ nat_div2.comp $ nat_div2.comp snd)),
455 refine ((nat_strong_rec
456 (λ a n, F a (of_nat code n)) this.to₂ $ λ a n, _).comp
id ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘
typ ┴ ┴ ┴ └──┘ ┴ ┴
457 computable.id $ encode_iff.2 hc).of_eq (λ a, by simp),
id ┴
typ ┴
458 simp,
459 iterate 4 {cases n with n, {refl}},
id ┴
typ ┴
st ┴
460 simp [G], rw [list.length_map, list.length_range],
461 let m := n.div2.div2,
id └─────────┘
src └─────────┘
typ └─────────┘
462 show G₁ ((a, (list.range (n+4)).map (λ n, F a (of_nat code n))), n, m)
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
463 = some (F a (of_nat code (n+4))),
id ┴ └──┘ ┴
src └──┘
typ ┴ └──┘ ┴
464 have hm : m < n + 4, by simp [nat.div2_val, m];
id ┴ ┴ ┴
typ ┴ ┴ ┴
465 from lt_of_le_of_lt
466 (le_trans (nat.div_le_self _ _) (nat.div_le_self _ _))
467 (nat.succ_le_succ (nat.le_add_right _ _)),
468 have m1 : m.unpair.1 < n + 4, from lt_of_le_of_lt m.unpair_le_left hm,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
469 have m2 : m.unpair.2 < n + 4, from lt_of_le_of_lt m.unpair_le_right hm,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
470 simp [G₁], simp [list.nth_map, list.nth_range, hm, m1, m2],
471 change of_nat code (n+4) with of_nat_code (n+4),
id └──┘ ┴ └─────────┘ ┴
src └──┘ └─────────┘
typ └──┘ ┴ └─────────┘ ┴
472 simp [of_nat_code],
id └─────────┘
src └─────────┘
typ └─────────┘
473 cases n.bodd; cases n.div2.bodd; refl
id └────┘ └──┘
src └────┘ └──┘
typ └────┘ └──┘
doc └──┘
474 end
st └─┘
475
476 end
477
478 def eval : code → ℕ →. ℕ
id └──┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴
479 | zero := pure 0
id └──┘
src └──┘
typ └──┘
480 | succ := nat.succ
id └──┘ └┘ └┘
src └──┘ └┘ └┘
typ └──┘ └┘ └┘
481 | left := λ n, n.unpair.1
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
482 | right := λ n, n.unpair.2
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
483 | (pair cf cg) := λ n, mkpair <$> eval cf n <*> eval cg n
id ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
484 | (comp cf cg) := λ n, eval cg n >>= eval cf
id └──┘ └┘ └┘ └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ └┘ └┘ └──┘ ┴ ┴ ┴
485 | (prec cf cg) := nat.unpaired (λ a n,
id └──┘ └┘ └┘ ┴ ┴
src └──┘
typ └──┘ └┘ └┘ ┴ ┴
486 n.elim (eval cf a) (λ y IH, do i ← IH, eval cg (mkpair a (mkpair y i))))
id ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └──┘ └────┘ ┴ └────┘ ┴ ┴
src └────┘ └────┘
typ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └──┘ └────┘ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
487 | (rfind' cf) := nat.unpaired (λ a m,
id └────┘ └┘ ┴ ┴
src └────┘
typ └────┘ └┘ ┴ ┴
488 (nat.rfind (λ n, (λ m, m = 0) <$>
id ┴ ┴ ┴
typ ┴ ┴ ┴
489 eval cf (mkpair a (n + m)))).map (+ m))
id └──┘ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴
490
491 instance : has_mem (ℕ →. ℕ) code := ⟨λ f c, eval c = f⟩
id ┴ └┘ ┴ └──┘ ┴ ┴ ┴
src ┴ └┘ ┴ └──┘
typ ┴ └┘ ┴ └──┘ ┴ ┴ ┴
doc └┘
492
493 @[simp] theorem eval_const : ∀ n m, eval (code.const n) m = roption.some n
id ┴ └┘ └┘ └┘ ┴ ┴ ┴
src └┘ └┘ └┘
typ ┴ └┘ └┘ └┘ ┴ ┴ ┴
doc └──┘
494 | 0 m := rfl
495 | (n+1) m := by simp! *
496
497 @[simp] theorem eval_id (n) : eval code.id n = roption.some n := by simp! [(<*>)]
id └─────┘ ┴ ┴
src └─────┘
typ └─────┘ ┴ ┴
doc └──┘
498
499 @[simp] theorem eval_curry (c n x) : eval (curry c n) x = eval c (mkpair n x) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
500 by simp! [(<*>)]
501
502 theorem const_prim : primrec code.const :=
id └┘ └┘ └┘
src └┘ └┘ └┘
typ └┘ └┘ └┘
503 (primrec.id.nat_iterate (primrec.const zero)
id └──┘
src └──┘
typ └──┘
504 (comp_prim.comp (primrec.const succ) primrec.snd).to₂).of_eq $
id └──┘
src └──┘
typ └──┘
505 λ n, by simp; induction n; simp [*, code.const, nat.iterate_succ']
id ┴ ┴ └────────┘
src └────────┘
typ ┴ ┴ └────────┘
506
507 theorem curry_prim : primrec₂ curry :=
508 comp_prim.comp primrec.fst $
509 pair_prim.comp (const_prim.comp primrec.snd) (primrec.const code.id)
id └─────┘
src └─────┘
typ └─────┘
510
511 theorem exists_code {f : ℕ →. ℕ} : nat.partrec f ↔ ∃ c : code, eval c = f :=
id ┴ └┘ ┴ ┴ └──┘ ┴ ┴
src ┴ └┘ ┴ └──┘
typ ┴ └┘ ┴ ┴ └──┘ ┴ ┴
doc └┘
512 ⟨λ h, begin
513 induction h,
514 case nat.partrec.zero { exact ⟨zero, rfl⟩ },
id └──┘
src └──┘
typ └──┘
st └┘
515 case nat.partrec.succ { exact ⟨succ, rfl⟩ },
id └──┘
src └──┘
typ └──┘
st └┘
516 case nat.partrec.left { exact ⟨left, rfl⟩ },
id └──┘
src └──┘
typ └──┘
st └┘
517 case nat.partrec.right { exact ⟨right, rfl⟩ },
id └───┘
src └───┘
typ └───┘
st └┘
518 case nat.partrec.pair : f g pf pg hf hg {
519 rcases hf with ⟨cf, rfl⟩, rcases hg with ⟨cg, rfl⟩,
520 exact ⟨pair cf cg, rfl⟩ },
id └──┘ └┘ └┘
src └──┘
typ └──┘ └┘ └┘
st └┘
521 case nat.partrec.comp : f g pf pg hf hg {
522 rcases hf with ⟨cf, rfl⟩, rcases hg with ⟨cg, rfl⟩,
523 exact ⟨comp cf cg, rfl⟩ },
id └──┘ └┘ └┘
src └──┘
typ └──┘ └┘ └┘
st └┘
524 case nat.partrec.prec : f g pf pg hf hg {
525 rcases hf with ⟨cf, rfl⟩, rcases hg with ⟨cg, rfl⟩,
526 exact ⟨prec cf cg, rfl⟩ },
id └──┘ └┘ └┘
src └──┘
typ └──┘ └┘ └┘
st └┘
527 case nat.partrec.rfind : f pf hf {
528 rcases hf with ⟨cf, rfl⟩,
529 refine ⟨comp (rfind' cf) (pair code.id zero), _⟩,
id └──┘ └────┘ └┘ └──┘ └─────┘ └──┘
src └──┘ └────┘ └──┘ └─────┘ └──┘
typ └──┘ └────┘ └┘ └──┘ └─────┘ └──┘
530 simp [eval, (<*>), pure, pfun.pure, roption.map_id'] },
id └──┘
src └──┘
typ └──┘
st └┘
531 end, λ h, begin
st └─┘
532 rcases h with ⟨c, rfl⟩, induction c,
id ┴
typ ┴
533 case nat.partrec.code.zero { exact nat.partrec.zero },
st ┴ └┘
534 case nat.partrec.code.succ { exact nat.partrec.succ },
st ┴ └┘
535 case nat.partrec.code.left { exact nat.partrec.left },
st ┴ └┘
536 case nat.partrec.code.right { exact nat.partrec.right },
st ┴ └┘
537 case nat.partrec.code.pair : cf cg pf pg { exact pf.pair pg },
id └┘
typ └┘
st └┘
538 case nat.partrec.code.comp : cf cg pf pg { exact pf.comp pg },
id └┘
typ └┘
st └┘
539 case nat.partrec.code.prec : cf cg pf pg { exact pf.prec pg },
id └┘
typ └┘
st └┘
540 case nat.partrec.code.rfind' : cf pf { exact pf.rfind' },
st └┘
541 end⟩
st └─┘
542
543 def evaln : ∀ k : ℕ, code → ℕ → option ℕ
id ┴ └──┘ ┴ ┴
src ┴ └──┘ ┴ ┴
typ ┴ └──┘ ┴ ┴
544 | 0 _ := λ m, none
id ┴
typ ┴
545 | (k+1) zero := λ n, guard (n ≤ k) >> pure 0
id ┴ └──┘ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴
546 | (k+1) succ := λ n, guard (n ≤ k) >> pure (nat.succ n)
id ┴ └──┘ ┴ ┴ └──────┘ ┴
src └──┘ └──────┘
typ ┴ └──┘ ┴ ┴ └──────┘ ┴
547 | (k+1) left := λ n, guard (n ≤ k) >> pure n.unpair.1
id ┴ └──┘ ┴ ┴ ┴└─────┘
src └──┘ └─────┘
typ ┴ └──┘ ┴ ┴ ┴└─────┘
doc └─────┘
548 | (k+1) right := λ n, guard (n ≤ k) >> pure n.unpair.2
id ┴ └───┘ ┴ ┴ ┴└─────┘
src └───┘ └─────┘
typ ┴ └───┘ ┴ ┴ ┴└─────┘
doc └─────┘
549 | (k+1) (pair cf cg) := λ n, guard (n ≤ k) >>
id ┴ └──┘ └┘ └┘ ┴ ┴
src └──┘
typ ┴ └──┘ └┘ └┘ ┴ ┴
550 mkpair <$> evaln (k+1) cf n <*> evaln (k+1) cg n
id ┴ ┴
typ ┴ ┴
551 | (k+1) (comp cf cg) := λ n, guard (n ≤ k) >>
id ┴ └──┘ └┘ └┘ ┴ ┴
src └──┘
typ ┴ └──┘ └┘ └┘ ┴ ┴
552 do x ← evaln (k+1) cg n, evaln (k+1) cf x
id ┴ ┴ ┴
typ ┴ ┴ ┴
553 | (k+1) (prec cf cg) := λ n, guard (n ≤ k) >>
id ┴ └──┘ └┘ └┘ ┴ ┴
src └──┘
typ ┴ └──┘ └┘ └┘ ┴ ┴
554 n.unpaired (λ a n,
id ┴ ┴ ┴
typ ┴ ┴ ┴
555 n.cases (evaln (k+1) cf a) $ λ y, do
id ┴ ┴ ┴
typ ┴ ┴ ┴
556 i ← evaln k (prec cf cg) (mkpair a y),
id ┴ ┴ ┴
typ ┴ ┴ ┴
557 evaln (k+1) cg (mkpair a (mkpair y i)))
id └────┘ ┴ └────┘ ┴ ┴
src └────┘ └────┘
typ └────┘ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
558 | (k+1) (rfind' cf) := λ n, guard (n ≤ k) >>
id ┴ └────┘ └┘ ┴ ┴
src └────┘
typ ┴ └────┘ └┘ ┴ ┴
559 n.unpaired (λ a m, do
id ┴ ┴ ┴
typ ┴ ┴ ┴
560 x ← evaln (k+1) cf (mkpair a m),
id ┴ ┴ ┴
typ ┴ ┴ ┴
561 if x = 0 then pure m else
id ┴ ┴
typ ┴ ┴
562 evaln k (rfind' cf) (mkpair a (m+1)))
id └────┘ └────┘ ┴ ┴
src └────┘ └────┘
typ └────┘ └────┘ ┴ ┴
doc └────┘
563 using_well_founded wf_tacs
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
564
565 theorem evaln_bound : ∀ {k c n x}, x ∈ evaln k c n → n < k
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
566 | 0 c n x h := by simp [evaln] at h; cases h
id ┴
typ ┴
567 | (k+1) c n x h := begin
568 suffices : ∀ {o : option ℕ}, x ∈ guard (n ≤ k) >> o → n < k + 1,
id └────┘ ┴ ┴ ┴
src └────┘
typ └────┘ ┴ ┴ ┴
569 { cases c; rw [evaln] at h; exact this h },
id ┴
typ ┴
st └┘
570 simp [(>>)], exact λ _ h _, nat.lt_succ_of_le h
id ┴ ┴
typ ┴ ┴
571 end
st └─┘
572
573 theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c n → x ∈ evaln k₂ c n
id └┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
typ └┘ └┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
574 | 0 k₂ c n x hl h := by simp [evaln] at h; cases h
id ┴
typ ┴
575 | (k+1) (k₂+1) c n x hl h := begin
576 have hl' := nat.le_of_succ_le_succ hl,
577 have : ∀ {k k₂ n x : ℕ} {o₁ o₂ : option ℕ},
578 k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) → x ∈ guard (n ≤ k) >> o₁ → x ∈ guard (n ≤ k₂) >> o₂,
579 { simp [(>>)], introv h h₁ h₂ h₃, exact ⟨le_trans h₂ h, h₁ h₃⟩ },
id └┘ ┴
typ └┘ ┴
st └┘
580 simp at h ⊢,
581 induction c with cf cg hf hg cf cg hf hg cf cg hf hg cf hf generalizing x n;
id ┴
typ ┴
582 rw [evaln] at h ⊢; refine this hl' (λ h, _) h,
583 iterate 4 {exact h},
584 { -- pair cf cg
585 simp [(<*>)] at h ⊢,
586 exact h.imp (λ a, and.imp
id ┴
typ ┴
587 (Exists.imp (λ b, and.imp_left (hf _ _)))
id ┴
typ ┴
588 (Exists.imp (λ b, and.imp_left (hg _ _)))) },
id ┴
typ ┴
st └┘
589 { -- comp cf cg
590 simp at h ⊢,
591 exact h.imp (λ a, and.imp (hg _ _) (hf _ _)) },
id ┴
typ ┴
st └┘
592 { -- prec cf cg
593 revert h, simp,
594 induction n.unpair.2; simp,
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
595 { apply hf },
st └┘
596 { exact λ y h₁ h₂, ⟨y, evaln_mono hl' h₁, hg _ _ h₂⟩ } },
id ┴ └─┘
typ ┴ └─┘
st └──┘
597 { -- rfind' cf
598 simp at h ⊢,
599 refine h.imp (λ x, and.imp (hf _ _) _),
id ┴
typ ┴
600 by_cases x0 : x = 0; simp [x0],
id ┴
typ ┴
601 exact evaln_mono hl' }
id └─┘
typ └─┘
st └─
602 end
st ──┘
603
604 theorem evaln_sound : ∀ {k c n x}, x ∈ evaln k c n → x ∈ eval c n
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
605 | 0 _ n x h := by simp [evaln] at h; cases h
id ┴
typ ┴
606 | (k+1) c n x h := begin
607 induction c with cf cg hf hg cf cg hf hg cf cg hf hg cf hf generalizing x n;
id ┴
typ ┴
608 simp [eval, evaln, (>>), (<*>)] at h ⊢; cases h with _ h,
609 iterate 4 {simpa [pure, pfun.pure, eq_comm] using h},
610 { -- pair cf cg
611 rcases h with ⟨_, ⟨y, ef, rfl⟩, z, eg, rfl⟩,
612 exact ⟨_, hf _ _ ef, _, hg _ _ eg, rfl⟩ },
st └┘
613 { --comp hf hg
614 rcases h with ⟨y, eg, ef⟩,
615 exact ⟨_, hg _ _ eg, hf _ _ ef⟩ },
st └┘
616 { -- prec cf cg
617 revert h,
618 induction n.unpair.2 with m IH generalizing x; simp,
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
619 { apply hf },
st └┘
620 { refine λ y h₁ h₂, ⟨y, IH _ _, _⟩,
id ┴
typ ┴
621 { have := evaln_mono k.le_succ h₁,
622 simp [evaln, (>>)] at this,
623 exact this.2 },
st └┘
624 { exact hg _ _ h₂ } } },
st └────┘
625 { -- rfind' cf
626 rcases h with ⟨m, h₁, h₂⟩,
627 by_cases m0 : m = 0; simp [m0] at h₂,
id ┴
typ ┴
628 { exact ⟨0,
629 ⟨by simpa [m0] using hf _ _ h₁,
630 λ m, (nat.not_lt_zero _).elim⟩,
id ┴
typ ┴
631 by injection h₂ with h₂; simp [h₂]⟩ },
st └┘
632 { have := evaln_sound h₂, simp [eval] at this,
id └──┘
src └──┘
typ └──┘
633 rcases this with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩,
634 refine ⟨y+1, ⟨by simpa using hy₁, λ i im, _⟩, by simp⟩,
id ┴ ┴
typ ┴ ┴
635 cases i with i,
id ┴
typ ┴
636 { exact ⟨m, by simpa using hf _ _ h₁, m0⟩ },
id ┴
typ ┴
st └┘
637 { rcases hy₂ (nat.lt_of_succ_lt_succ im) with ⟨z, hz, z0⟩,
638 exact ⟨z, by simpa [nat.succ_eq_add_one] using hz, z0⟩ } } }
id ┴
typ ┴
st └─────
639 end
st ──┘
640
641 theorem evaln_complete {c n x} : x ∈ eval c n ↔ ∃ k, x ∈ evaln k c n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
642 ⟨λ h, begin
643 suffices : ∃ k, x ∈ evaln (k+1) c n,
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
644 { exact let ⟨k, h⟩ := this in ⟨k+1, h⟩ },
id ┴
typ ┴
st └┘
645 induction c generalizing n x;
id ┴
typ ┴
646 simp [eval, evaln, pure, pfun.pure, (<*>), (>>)] at h ⊢,
647 iterate 4 { exact ⟨⟨_, le_refl _⟩, h.symm⟩ },
648 case nat.partrec.code.pair : cf cg hf hg {
649 rcases h with ⟨x, hx, y, hy, rfl⟩,
650 rcases hf hx with ⟨k₁, hk₁⟩, rcases hg hy with ⟨k₂, hk₂⟩,
651 refine ⟨max k₁ k₂, _⟩,
id └┘ └┘
typ └┘ └┘
652 exact ⟨le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁, _,
653 ⟨_, evaln_mono (nat.succ_le_succ $ le_max_left _ _) hk₁, rfl⟩,
654 _, evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk₂, rfl⟩ },
st └┘
655 case nat.partrec.code.comp : cf cg hf hg {
656 rcases h with ⟨y, hy, hx⟩,
657 rcases hg hy with ⟨k₁, hk₁⟩, rcases hf hx with ⟨k₂, hk₂⟩,
658 refine ⟨max k₁ k₂, _⟩,
id └┘ └┘
typ └┘ └┘
659 exact ⟨le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁, _,
660 evaln_mono (nat.succ_le_succ $ le_max_left _ _) hk₁,
661 evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk₂⟩ },
st └┘
662 case nat.partrec.code.prec : cf cg hf hg {
663 revert h,
664 generalize : n.unpair.1 = n₁, generalize : n.unpair.2 = n₂,
id └──────┘ └──────┘
src └──────┘ └──────┘
typ └──────┘ └──────┘
doc └──────┘ └──────┘
665 induction n₂ with m IH generalizing x n; simp,
id └┘
typ └┘
666 { intro, rcases hf h with ⟨k, hk⟩,
667 exact ⟨_, le_max_left _ _,
668 evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk⟩ },
st └┘
669 { intros y hy hx,
670 rcases IH hy with ⟨k₁, nk₁, hk₁⟩, rcases hg hx with ⟨k₂, hk₂⟩,
671 refine ⟨(max k₁ k₂).succ, nat.le_succ_of_le $ le_max_left_of_le $
id └┘ └┘ └──┘
src └──┘
typ └┘ └┘ └──┘
672 le_trans (le_max_left _ (mkpair n₁ m)) nk₁, y,
id └────┘ └┘ ┴ ┴
src └────┘
typ └────┘ └┘ ┴ ┴
doc └────┘
673 evaln_mono (nat.succ_le_succ $ le_max_left _ _) _,
674 evaln_mono (nat.succ_le_succ $ nat.le_succ_of_le $ le_max_right _ _) hk₂⟩,
675 simp [evaln, (>>)],
676 exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩ } },
st └──┘
677 case nat.partrec.code.rfind' : cf hf {
678 rcases h with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩,
679 suffices : ∃ k, y + n.unpair.2 ∈ evaln (k+1) (rfind' cf)
id ┴ ┴ └────┘ └┘
src └────┘
typ ┴ ┴ └────┘ └┘
680 (mkpair n.unpair.1 n.unpair.2), {simpa [evaln, (>>)]},
id └────┘
src └────┘
typ └────┘
doc └────┘
st └┘
681 revert hy₁ hy₂, generalize : n.unpair.2 = m, intros,
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
682 induction y with y IH generalizing m; simp [evaln, (>>)],
id ┴
typ ┴
683 { simp at hy₁, rcases hf hy₁ with ⟨k, hk⟩,
684 exact ⟨_, nat.le_of_lt_succ $ evaln_bound hk, _, hk, by simp; refl⟩ },
id └──┘
src └──┘
typ └──┘
doc └──┘
st └┘
685 { rcases hy₂ (nat.succ_pos _) with ⟨a, ha, a0⟩,
686 rcases hf ha with ⟨k₁, hk₁⟩,
687 rcases IH m.succ
id └────┘
src └────┘
typ └────┘
688 (by simpa [nat.succ_eq_add_one] using hy₁)
689 (λ i hi, by simpa [nat.succ_eq_add_one] using hy₂ (nat.succ_lt_succ hi))
id ┴ └┘ └┘
typ ┴ └┘ └┘
690 with ⟨k₂, hk₂⟩,
691 simp at hk₁,
692 exact ⟨(max k₁ k₂).succ, nat.le_succ_of_le $
id └┘ └┘ └──┘
src └──┘
typ └┘ └┘ └──┘
693 le_max_left_of_le $ nat.le_of_lt_succ $ evaln_bound hk₁, a,
id ┴
typ ┴
694 evaln_mono (nat.succ_le_succ $ nat.le_succ_of_le $ le_max_left _ _) hk₁,
695 by simpa [nat.succ_eq_add_one, a0, -max_eq_left, -max_eq_right] using
696 evaln_mono (nat.succ_le_succ $ le_max_right _ _) hk₂⟩ } }
st └───
697 end, λ ⟨k, h⟩, evaln_sound h⟩
st ──┘
698
699 section
700 open primrec
701
702 private def lup (L : list (list (option ℕ))) (p : ℕ × code) (n : ℕ) :=
id └┘ └┘ └┘ └┘ ┴ ┴ └──┘ ┴
src └┘ └┘ └┘ └┘ ┴ ┴ └──┘ ┴
typ └┘ └┘ └┘ └┘ ┴ ┴ └──┘ ┴
703 do l ← L.nth (encode p), o ← l.nth n, o
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
704
705 private lemma hlup : primrec (λ p:_×(_×_)×_, lup p.1 p.2.1 p.2.2) :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
706 option_bind
707 (list_nth.comp fst (primrec.encode.comp $ fst.comp snd))
708 (option_bind (list_nth.comp snd $ snd.comp $ snd.comp fst) snd)
709
710 private def G (L : list (list (option ℕ))) : option (list (option ℕ)) :=
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
711 option.some $
712 let a := of_nat (ℕ × code) L.length,
id ┴ ┴ ┴ └──┘
src ┴ ┴ └──┘
typ ┴ ┴ ┴ └──┘
713 k := a.1, c := a.2 in
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
714 (list.range k).map (λ n,
id ┴ ┴
typ ┴ ┴
715 k.cases none $ λ k',
id ┴ └┘
typ ┴ └┘
716 nat.partrec.code.rec_on c
id ┴
typ ┴
717 (some 0) -- zero
718 (some (nat.succ n))
id └┘ └┘ ┴
src └┘ └┘
typ └┘ └┘ ┴
719 (some n.unpair.1)
id ┴ └──┘
src └──┘
typ ┴ └──┘
doc └──┘
720 (some n.unpair.2)
id ┴ └──┘
src └──┘
typ ┴ └──┘
doc └──┘
721 (λ cf cg _ _, do
id └┘ └┘ ┴ ┴
typ └┘ └┘ ┴ ┴
722 x ← lup L (k, cf) n,
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
723 y ← lup L (k, cg) n,
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
724 some (mkpair x y))
id └──┘ ┴ ┴
src └──┘
typ └──┘ ┴ ┴
doc └──┘
725 (λ cf cg _ _, do
id └┘ └┘ ┴ ┴
typ └┘ └┘ ┴ ┴
726 x ← lup L (k, cg) n,
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
727 lup L (k, cf) x)
id ┴ └┘ ┴
typ ┴ └┘ ┴
728 (λ cf cg _ _,
id └┘ └┘ ┴ ┴
typ └┘ └┘ ┴ ┴
729 let z := n.unpair.1 in
id ┴ ┴└─────┘
src └─────┘
typ ┴ ┴└─────┘
doc └─────┘
730 n.unpair.2.cases
id ┴└─────┘
src └─────┘
typ ┴└─────┘
doc └─────┘
731 (lup L (k, cf) z)
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
732 (λ y, do
id ┴
typ ┴
733 i ← lup L (k', c) (mkpair z y),
id ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴
734 lup L (k, cg) (mkpair z (mkpair y i))))
id ┴ ┴ └┘ └────┘ ┴ └────┘ ┴ ┴
src └────┘ └────┘
typ ┴ ┴ └┘ └────┘ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
735 (λ cf _,
id └┘ ┴
typ └┘ ┴
736 let z := n.unpair.1, m := n.unpair.2 in do
id ┴ ┴└─────┘ ┴ ┴└─────┘
src └─────┘ └─────┘
typ ┴ ┴└─────┘ ┴ ┴└─────┘
doc └─────┘ └─────┘
737 x ← lup L (k, cf) (mkpair z m),
id ┴ ┴ ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴
738 x.cases
id ┴
typ ┴
739 (some m)
id ┴
typ ┴
740 (λ _, lup L (k', c) (mkpair z (m+1)))))
id ┴ ┴ └┘ ┴ └────┘ ┴ ┴
src └────┘
typ ┴ ┴ └┘ ┴ └────┘ ┴ ┴
doc └────┘
741
742 private lemma hG : primrec G :=
743 begin
744 have a := (primrec.of_nat (ℕ × code)).comp list_length,
id ┴ └──┘
src ┴ └──┘
typ ┴ └──┘
745 have k := fst.comp a,
746 refine option_some.comp
747 (list_map (list_range.comp k) (_ : primrec _)),
748 replace k := k.comp fst, have n := snd,
749 refine nat_cases k (const none) (_ : primrec _),
id └──┘
src └──┘
typ └──┘
750 have k := k.comp fst, have n := n.comp fst, have k' := snd,
751 have c := snd.comp (a.comp $ fst.comp fst),
752 apply rec_prim c
753 (const (some 0))
754 (option_some.comp (primrec.succ.comp n))
755 (option_some.comp (fst.comp $ primrec.unpair.comp n))
756 (option_some.comp (snd.comp $ primrec.unpair.comp n)),
757 { have L := (fst.comp fst).comp fst,
758 have k := k.comp fst, have n := n.comp fst,
759 have cf := fst.comp snd,
760 have cg := (fst.comp snd).comp snd,
761 exact option_bind
762 (hlup.comp $ L.pair $ (k.pair cf).pair n)
763 (option_map ((hlup.comp $
764 L.pair $ (k.pair cg).pair n).comp fst)
765 (primrec₂.mkpair.comp (snd.comp fst) snd)) },
st └┘
766 { have L := (fst.comp fst).comp fst,
767 have k := k.comp fst, have n := n.comp fst,
768 have cf := fst.comp snd,
769 have cg := (fst.comp snd).comp snd,
770 exact option_bind
771 (hlup.comp $ L.pair $ (k.pair cg).pair n)
772 (hlup.comp ((L.comp fst).pair $
773 ((k.pair cf).comp fst).pair snd)) },
st └┘
774 { have L := (fst.comp fst).comp fst,
775 have k := k.comp fst, have n := n.comp fst,
776 have cf := fst.comp snd,
777 have cg := (fst.comp snd).comp snd,
778 have z := fst.comp (primrec.unpair.comp n),
779 refine nat_cases
780 (snd.comp (primrec.unpair.comp n))
781 (hlup.comp $ L.pair $ (k.pair cf).pair z)
782 (_ : primrec _),
783 have L := L.comp fst, have z := z.comp fst, have y := snd,
784 refine option_bind
785 (hlup.comp $ L.pair $
786 (((k'.pair c).comp fst).comp fst).pair
787 (primrec₂.mkpair.comp z y))
788 (_ : primrec _),
789 have z := z.comp fst, have y := y.comp fst, have i := snd,
790 exact hlup.comp ((L.comp fst).pair $
791 ((k.pair cg).comp $ fst.comp fst).pair $
792 primrec₂.mkpair.comp z $ primrec₂.mkpair.comp y i) },
st └┘
793 { have L := (fst.comp fst).comp fst,
794 have k := k.comp fst, have n := n.comp fst,
795 have cf := fst.comp snd,
796 have z := fst.comp (primrec.unpair.comp n),
797 have m := snd.comp (primrec.unpair.comp n),
798 refine option_bind
799 (hlup.comp $ L.pair $ (k.pair cf).pair (primrec₂.mkpair.comp z m))
800 (_ : primrec _),
801 have m := m.comp fst,
802 exact nat_cases snd (option_some.comp m)
803 ((hlup.comp ((L.comp fst).pair $
804 ((k'.pair c).comp $ fst.comp fst).pair
805 (primrec₂.mkpair.comp (z.comp fst)
806 (primrec.succ.comp m)))).comp fst) }
st └─
807 end
st ──┘
808
809 private lemma evaln_map (k c n) :
810 (((list.range k).nth n).map (evaln k c)).bind (λ b, b) = evaln k c n :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
811 begin
812 by_cases kn : n < k,
813 { simp [list.nth_range kn] },
id └┘
typ └┘
st └┘
814 { rw list.nth_len_le,
815 { cases e : evaln k c n, {refl},
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └┘
816 exact kn.elim (evaln_bound e) },
st └┘
817 simpa using kn }
id └┘
typ └┘
st └─
818 end
st ──┘
819
820 theorem evaln_prim : primrec (λ (a : (ℕ × code) × ℕ), evaln a.1.1 a.1.2 a.2) :=
id ┴ ┴ └──┘ ┴
src ┴ ┴ └──┘ ┴
typ ┴ ┴ └──┘ ┴
821 have primrec₂ (λ (_:unit) (n : ℕ),
id └──┘ ┴
src └──┘ ┴
typ └──┘ ┴
doc └──┘
822 let a := of_nat (ℕ × code) n in
id ┴ ┴ └──┘ ┴
src ┴ └──┘
typ ┴ ┴ └──┘ ┴
823 (list.range a.1).map (evaln a.1 a.2)), from
id ┴ ┴
typ ┴ ┴
824 primrec.nat_strong_rec _ (hG.comp snd).to₂ $
825 λ _ p, begin
id ┴ ┴
typ ┴ ┴
826 simp [G],
827 rw (_ : (of_nat (ℕ × code) _).snd =
id ┴
src ┴
typ ┴
828 of_nat code p.unpair.2), swap, {simp},
id └──┘ └──────┘
src └──┘ └──────┘
typ └──┘ └──────┘
doc └──────┘
st └┘
829 apply list.map_congr (λ n, _),
id ┴
typ ┴
830 rw (by simp : list.range p = list.range
831 (mkpair p.unpair.1 (encode (of_nat code p.unpair.2)))),
id └────┘ └──┘
src └────┘ └──┘
typ └────┘ └──┘
doc └────┘
832 generalize : p.unpair.1 = k,
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
833 generalize : of_nat code p.unpair.2 = c,
id └──┘ └──────┘
src └──┘ └──────┘
typ └──┘ └──────┘
doc └──────┘
834 intro nk,
835 cases k with k', {simp [evaln]},
id ┴
typ ┴
st └┘
836 let k := k'+1, change k'.succ with k,
id └┘ └─────┘ ┴
src └─────┘
typ └┘ └─────┘ ┴
837 simp [nat.lt_succ_iff] at nk,
838 have hg : ∀ {k' c' n},
id └┘ └┘ ┴
typ └┘ └┘ ┴
839 mkpair k' (encode c') < mkpair k (encode c) →
840 lup ((list.range (mkpair k (encode c))).map (λ n,
id ┴ ┴ ┴
typ ┴ ┴ ┴
841 (list.range n.unpair.1).map
842 (evaln n.unpair.1 (of_nat code n.unpair.2))))
id └──┘
src └──┘
typ └──┘
843 (k', c') n = evaln k' c' n,
844 { intros k₁ c₁ n₁ hl,
845 simp [lup, list.nth_range hl, evaln_map, (>>=)] },
st └┘
846 cases c with cf cg cf cg cf cg cf;
id ┴
typ ┴
847 simp [evaln, nk, (>>), (>>=), (<$>), (<*>), pure],
848 { cases encode_lt_pair cf cg with lf lg,
id └┘ └┘
typ └┘ └┘
849 rw [hg (nat.mkpair_lt_mkpair_right _ lf),
850 hg (nat.mkpair_lt_mkpair_right _ lg)],
851 cases evaln k cf n, {refl},
id ┴ └┘ ┴
typ ┴ └┘ ┴
st └┘
852 cases evaln k cg n; refl },
id ┴ └┘ ┴ └──┘
src └──┘
typ ┴ └┘ ┴ └──┘
doc └──┘
st └┘
853 { cases encode_lt_comp cf cg with lf lg,
id └┘ └┘
typ └┘ └┘
854 rw hg (nat.mkpair_lt_mkpair_right _ lg),
855 cases evaln k cg n, {refl},
id ┴ └┘ ┴
typ ┴ └┘ ┴
st └┘
856 simp [hg (nat.mkpair_lt_mkpair_right _ lf)] },
st └┘
857 { cases encode_lt_prec cf cg with lf lg,
id └┘ └┘
typ └┘ └┘
858 rw hg (nat.mkpair_lt_mkpair_right _ lf),
859 cases n.unpair.2, {refl},
id └──────┘
src └──────┘
typ └──────┘
doc └──────┘
st └┘
860 simp,
861 rw hg (nat.mkpair_lt_mkpair_left _ k'.lt_succ_self),
862 cases evaln k' _ _, {refl},
id └┘
typ └┘
st └┘
863 simp [hg (nat.mkpair_lt_mkpair_right _ lg)] },
st └┘
864 { have lf := encode_lt_rfind' cf,
id └┘
typ └┘
865 rw hg (nat.mkpair_lt_mkpair_right _ lf),
866 cases evaln k cf n with x, {refl},
id ┴ └┘ ┴
typ ┴ └┘ ┴
st └┘
867 simp,
868 cases x; simp [nat.succ_ne_zero],
id ┴
typ ┴
869 rw hg (nat.mkpair_lt_mkpair_left _ k'.lt_succ_self) }
st └┘
870 end,
st └─┘
871 (option_bind (list_nth.comp
872 (this.comp (const ()) (encode_iff.2 fst)) snd)
id └┘
src └┘
typ └┘
873 snd.to₂).of_eq $ λ ⟨⟨k, c⟩, n⟩, by simp [evaln_map]
874
875 end
876
877 section
878 open partrec computable
879
880 theorem eval_eq_rfind_opt (c n) :
881 eval c n = nat.rfind_opt (λ k, evaln k c n) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
882 roption.ext $ λ x, begin
id ┴
typ ┴
883 refine evaln_complete.trans (nat.rfind_opt_mono _).symm,
884 intros a m n hl, apply evaln_mono hl,
id └┘
typ └┘
885 end
st └─┘
886
887 theorem eval_part : partrec₂ eval :=
888 (rfind_opt (evaln_prim.to_comp.comp
889 ((snd.pair (fst.comp fst)).pair (snd.comp fst))).to₂).of_eq $
890 λ a, by simp [eval_eq_rfind_opt]
id ┴
typ ┴
891
892 theorem fixed_point
893 {f : code → code} (hf : computable f) : ∃ c : code, eval (f c) = eval c :=
id └──┘ └──┘ ┴ └──┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘
typ └──┘ └──┘ ┴ └──┘ ┴ ┴ ┴
894 let g (x y : ℕ) : roption ℕ :=
id ┴ ┴
src ┴ ┴
typ ┴ ┴
895 eval (of_nat code x) x >>= λ b, eval (of_nat code b) y in
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ └──┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
896 have partrec₂ g :=
897 (eval_part.comp ((computable.of_nat _).comp fst) fst).bind
898 (eval_part.comp ((computable.of_nat _).comp snd) (snd.comp fst)).to₂,
899 let ⟨cg, eg⟩ := exists_code.1 this in
id └┘
typ └┘
900 have eg' : ∀ a n, eval cg (mkpair a n) = roption.map encode (g a n) :=
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
901 by simp [eg],
902 let F (x : ℕ) : code := f (curry cg x) in
id ┴ └──┘ ┴ ┴
src ┴ └──┘
typ ┴ └──┘ ┴ ┴
903 have computable F :=
id ┴
typ ┴
904 hf.comp (curry_prim.comp (primrec.const cg) primrec.id).to_comp,
905 let ⟨cF, eF⟩ := exists_code.1 this in
id └┘
typ └┘
906 have eF' : eval cF (encode cF) = roption.some (encode (F (encode cF))),
id ┴
typ ┴
907 by simp [eF],
908 ⟨curry cg (encode cF), funext (λ n,
id ┴
typ ┴
909 show eval (f (curry cg (encode cF))) n = eval (curry cg (encode cF)) n,
id ┴ ┴ ┴
typ ┴ ┴ ┴
910 by simp [eg', eF', roption.map_id', g])⟩
id ┴
typ ┴
911
912 theorem fixed_point₂
913 {f : code → ℕ →. ℕ} (hf : partrec₂ f) : ∃ c : code, eval c = f c :=
id └──┘ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ └┘ ┴ └──┘
typ └──┘ ┴ └┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └┘
914 let ⟨cf, ef⟩ := exists_code.1 hf in
id └┘
typ └┘
915 (fixed_point (curry_prim.comp
916 (primrec.const cf) primrec.encode).to_comp).imp $
917 λ c e, funext $ λ n, by simp [e.symm, ef, roption.map_id']
id ┴ ┴
typ ┴ ┴
918
919 end
920
921 end nat.partrec.code